1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5 -/
6
7 import field_theory.finite data.zmod.basic data.nat.parity
src └─────────────────┘ └─────────────┘ └─────────────┘
8
9 /-!
10 # Quadratic reciprocity.
11
12 This file contains results about quadratic residues modulo a prime number.
13
14 The main results are the law of quadratic reciprocity, `quadratic_reciprocity`, as well as the
15 interpretations in terms of existence of square roots depending on the congruence mod 4,
16 `exists_pow_two_eq_prime_iff_of_mod_four_eq_one`, and
17 `exists_pow_two_eq_prime_iff_of_mod_four_eq_three`.
18
19 Also proven are conditions for `-1` and `2` to be a square modulo a prime,
20 `exists_pow_two_eq_neg_one_iff_mod_four_ne_three` and
21 `exists_pow_two_eq_two_iff`
22
23 ## Implementation notes
24
25 The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein's lemma
26 -/
27
28
29 open function finset nat finite_field zmodp
30
31 namespace zmodp
32
33 variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
id ┴ └───────┘ └───────┘
src ┴ └───────┘ └───────┘
typ ┴ └───────┘ └───────┘
doc └───────┘ └───────┘
34
35 @[simp] lemma card_units_zmodp : fintype.card (units (zmodp p hp)) = p - 1 :=
id └──────────┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴
src └──────────┘ └───┘ └───┘ ┴ ┴
typ └──────────┘ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──────────┘
36 by rw [card_units, card_zmodp]
id └────────┘ └────────┘
src └──┘└────────┘└┘└────────┘└─
typ └──┘└────────┘└┘└────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└──────────┘┴└
37
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
38 theorem fermat_little {p : ℕ} (hp : nat.prime p) {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p - 1) = 1 :=
id ┴ └───────┘ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴
typ ┴ └───────┘ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
39 by rw [← units.mk0_val ha, ← @units.coe_one (zmodp p hp), ← units.coe_pow, ← units.ext_iff,
id └───────────┘ └┘ └───────────┘ └───┘ ┴ └┘ └───────────┘ └───────────┘
src └────┘└───────────┘┴ └──┘ └───────────┘┴ └───┘┴ ┴ └───┘└───────────┘└──┘└───────────┘└─
typ └────┘└───────────┘┴└┘└──┘ └───────────┘┴ └───┘┴┴┴└┘└───┘└───────────┘└──┘└───────────┘└─
doc └────┘ ┴ └──┘ ┴ ┴ ┴ └───┘ └──┘ └─
txt └────┘ ┴ └──┘ ┴ ┴ ┴ └───┘ └──┘ └─
par └────┘ ┴ └──┘ ┴ ┴ ┴ └───┘ └──┘ └─
pid └──┘ ┴ └──┘ ┴ ┴ ┴ └───┘ └──┘ └─
st └─────────────────────┘└─────────────────────────────┘└───────────────┘└───────────────┘└─
40 ← card_units_zmodp hp, pow_card_eq_one]
id └──────────────┘ └┘ └─────────────┘
src ─────┘└──────────────┘┴ └┘└─────────────┘└─
typ ─────┘└──────────────┘┴└┘└┘└─────────────┘└─
doc ─────┘ ┴ └┘ └─
txt ─────┘ ┴ └┘ └─
par ─────┘ ┴ └┘ └─
pid ─────┘ ┴ └┘ ┴└
st ────────────────────────┘└───────────────┘┴└
41
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
42 lemma euler_criterion_units {x : units (zmodp p hp)} :
id └───┘ └───┘ ┴ └┘
src └───┘ └───┘
typ └───┘ └───┘ ┴ └┘
43 (∃ y : units (zmodp p hp), y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
id ┴ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
44 hp.eq_two_or_odd.elim
id └┘└────────────┘└───┘
src └────────────┘└───┘
typ └┘└────────────┘└───┘
45 (λ h, by resetI; subst h; revert x; exact dec_trivial)
id ┴ ┴ └─────────┘
src └────┘ └────┘ └──────┘ └────┘└─────────┘
typ ┴ └────┘ └────┘┴ └──────┘ └────┘└─────────┘
doc └────┘ └────┘ └──────┘ └────┘└─────────┘
txt └────┘ └────┘ └──────┘ └────┘
par └────┘ └────┘ └──────┘ └────┘
pid ┴ └┘ ┴
st └───────────────────────────────────────────┘
46 (λ hp1, let ⟨g, hg⟩ := is_cyclic.exists_generator (units (zmodp p hp)) in
id └─┘ └─┘ ┴ └┘ └────────────────────────┘ └───┘ └───┘ ┴ └┘
src └────────────────────────┘ └───┘ └───┘
typ └─┘ └─┘ ┴ └┘ └────────────────────────┘ └───┘ └───┘ ┴ └┘
47 let ⟨n, hn⟩ := show x ∈ powers g, from (powers_eq_gpowers g).symm ▸ hg x in
id └─┘ ┴ ┴ ┴ └────┘ └───────────────┘ └──┘ ┴ ┴
src ┴ └────┘ └───────────────┘ └──┘ ┴
typ └─┘ ┴ ┴ ┴ └────┘ └───────────────┘ └──┘ ┴ ┴
doc └────┘
48 ⟨λ ⟨y, hy⟩, by rw [← hy, ← pow_mul, two_mul_odd_div_two hp1,
id ┴ └┘ └─────┘ └─────────────────┘ └─┘
src └────┘ └──┘└─────┘└┘└─────────────────┘┴ └─
typ ┴ └────┘└┘└──┘└─────┘└┘└─────────────────┘┴└─┘└─
doc └────┘ └──┘ └┘ ┴ └─
txt └────┘ └──┘ └┘ ┴ └─
par └────┘ └──┘ └┘ ┴ └─
pid └──┘ └──┘ └┘ ┴ └─
st └───────┘└─────────┘└───────────────────────┘└─
49 ← card_units_zmodp hp, pow_card_eq_one],
id └──────────────┘ └┘ └─────────────┘
src ─────────┘└──────────────┘┴ └┘└─────────────┘┴
typ ─────────┘└──────────────┘┴└┘└┘└─────────────┘┴
doc ─────────┘ ┴ └┘ ┴
txt ─────────┘ ┴ └┘ ┴
par ─────────┘ ┴ └┘ ┴
pid ─────────┘ ┴ └┘ ┴
st ────────────────────────────┘└───────────────┘┴
50 λ hx, have 2 * (p / 2) ∣ n * (p / 2),
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
51 by rw [two_mul_odd_div_two hp1, ← card_units_zmodp hp, ← order_of_eq_card_of_forall_mem_gpowers hg];
id └─────────────────┘ └─┘ └──────────────┘ └┘ └────────────────────────────────────┘ └┘
src └──┘└─────────────────┘┴ └──┘└──────────────┘┴ └──┘└────────────────────────────────────┘┴ ┴
typ └──┘└─────────────────┘┴└─┘└──┘└──────────────┘┴└┘└──┘└────────────────────────────────────┘┴└┘┴
doc └──┘ ┴ └──┘ ┴ └──┘ ┴ ┴
txt └──┘ ┴ └──┘ ┴ └──┘ ┴ ┴
par └──┘ ┴ └──┘ ┴ └──┘ ┴ ┴
pid └┘ ┴ └──┘ ┴ └──┘ ┴ ┴
st └──────────────────────────┘└─────────────────────┘└───────────────────────────────────────────┘┴└─
52 exact order_of_dvd_of_pow_eq_one (by rwa [pow_mul, hn]),
id └────────────────────────┘ └─────┘ └┘
src └────┘└────────────────────────┘┴ ┴└───┘└─────┘└┘ ┴┴
typ └────┘└────────────────────────┘┴ ┴└───┘└─────┘└┘└┘┴┴
doc └────┘ ┴ ┴└───┘ └┘ ┴┴
txt └────┘ ┴ ┴└───┘ └┘ ┴┴
par └────┘ ┴ ┴└───┘ └┘ ┴┴
pid ┴ ┴ └────┘ └┘ └┘
st ───────────────────────────────────────────┘└───────────┘└──┘┴┴
53 let ⟨m, hm⟩ := dvd_of_mul_dvd_mul_right (nat.div_pos hp.two_le dec_trivial) this in
id └─┘ ┴ └──────────────────────┘ └─────────┘ └┘└─────┘ └─────────┘ └──┘
src └──────────────────────┘ └─────────┘ └─────┘ └─────────┘
typ └─┘ ┴ └──────────────────────┘ └─────────┘ └┘└─────┘ └─────────┘ └──┘
doc └─────────┘
54 ⟨g ^ m, by rwa [← pow_mul, mul_comm, ← hm]⟩⟩)
id ┴ └─────┘ └──────┘ └┘
src ┴ └─────┘└─────┘└┘└──────┘└──┘ ┴
typ ┴ └─────┘└─────┘└┘└──────┘└──┘└┘┴
doc └─────┘ └┘ └──┘ ┴
txt └─────┘ └┘ └──┘ ┴
par └─────┘ └┘ └──┘ ┴
pid └──┘ └┘ └──┘ ┴
st └─────────────┘└────────┘└────┘┴
55
56 lemma euler_criterion {a : zmodp p hp} (ha : a ≠ 0) :
id └───┘ ┴ └┘ ┴ ┴
src └───┘ ┴
typ └───┘ ┴ └┘ ┴ ┴
57 (∃ y : zmodp p hp, y ^ 2 = a) ↔ a ^ (p / 2) = 1 :=
id ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
58 ⟨λ ⟨y, hy⟩,
id ┴┴
typ ┴┴
59 have hy0 : y ≠ 0, from λ h, by simp [h, _root_.zero_pow (succ_pos 1)] at hy; cc,
id ┴ ┴ ┴ └─────────────┘ └──────┘
src ┴ └────┘ └┘└─────────────┘┴ └──────┘└────────┘ └┘
typ ┴ ┴ └────┘┴└┘└─────────────┘┴ └──────┘└────────┘ └┘
doc └────┘ └┘ ┴ └────────┘ └┘
txt └────┘ └┘ ┴ └────────┘ └┘
par └────┘ └┘ ┴ └────────┘ └┘
pid ┴┴ └┘ ┴ └──┘┴└───┘
st └───────────────────────────────────────────────┘
60 by simpa using (units.ext_iff.1 $ (euler_criterion_units hp).1 ⟨units.mk0 _ hy0, show _ = units.mk0 _ ha,
id └───────────┘ └───────────────────┘ └┘ └─┘ ┴ └───────┘ └┘
src └──────────┘ └───────────┘└─┘ ┴ └───────────────────┘┴ └──┘ └─┘ └┘ └─┘┴┴└───────┘└─┘ └─
typ └──────────┘ └───────────┘└─┘ ┴ └───────────────────┘┴└┘└──┘ └─┘└─┘└┘ └─┘┴┴└───────┘└─┘└┘└─
doc └──────────┘ └─┘ ┴ ┴ └──┘ └─┘ └┘ └─┘ ┴└───────┘└─┘ └─
txt └──────────┘ └─┘ ┴ ┴ └──┘ └─┘ └┘ └─┘ ┴ └─┘ └─
par └──────────┘ └─┘ ┴ ┴ └──┘ └─┘ └┘ └─┘ ┴ └─┘ └─
pid ┴└────┘ └─┘ ┴ ┴ └──┘ └─┘ └┘ └─┘ ┴ └─┘ └─
st └───────────────────────────────────────────────────────────────────────────────────────────────────────
61 by rw [units.ext_iff]; simpa⟩),
id └───────────┘
src ──────┘└──┘└───────────┘┴└───────┘
typ ──────┘└──┘└───────────┘┴└───────┘
doc ──────┘└──┘ ┴└───────┘
txt ──────┘└──┘ ┴└───────┘
par ──────┘└──┘ ┴└───────┘
pid ──────────┘ └────────┘
st ─────┘└────────────────┘┴└─────┘└┘
62 λ h, let ⟨y, hy⟩ := (euler_criterion_units hp).2 (show units.mk0 _ ha ^ (p / 2) = 1, by simpa [units.ext_iff]) in
id ┴ └─┘ ┴ └───────────────────┘ └┘ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────────┘
src └───────────────────┘ ┴ └───────┘ ┴ ┴ ┴ └─────┘└───────────┘┴
typ ┴ └─┘ ┴ └───────────────────┘ └┘ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └─────┘└───────────┘┴
doc └───────┘ └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └────────────────────┘
63 ⟨y, by simpa [units.ext_iff] using hy⟩⟩
id └───────────┘ └┘
src └─────┘└───────────┘└──────┘
typ └─────┘└───────────┘└──────┘└┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └─────────────────────────────┘
64
65 lemma exists_pow_two_eq_neg_one_iff_mod_four_ne_three :
66 (∃ y : zmodp p hp, y ^ 2 = -1) ↔ p % 4 ≠ 3 :=
id ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
67 have (-1 : zmodp p hp) ≠ 0, from mt neg_eq_zero.1 one_ne_zero,
id ┴ └───┘ ┴ └┘ ┴ └┘ └─────────┘┴ └─────────┘
src ┴ └───┘ ┴ └┘ └─────────┘┴ └─────────┘
typ ┴ └───┘ ┴ └┘ ┴ └┘ └─────────┘┴ └─────────┘
68 hp.eq_two_or_odd.elim (λ hp, by resetI; subst hp; exact dec_trivial)
id └┘└────────────┘└───┘ └┘ └┘ └─────────┘
src └────────────┘└───┘ └────┘ └────┘ └────┘└─────────┘
typ └┘└────────────┘└───┘ └┘ └────┘ └────┘└┘ └────┘└─────────┘
doc └────┘ └────┘ └────┘└─────────┘
txt └────┘ └────┘ └────┘
par └────┘ └────┘ └────┘
pid ┴ ┴
st └──────────────────────────────────┘
69 (λ hp1, (mod_two_eq_zero_or_one (p / 2)).elim
id └─┘ └────────────────────┘ ┴ ┴ └──┘
src └────────────────────┘ ┴ └──┘
typ └─┘ └────────────────────┘ ┴ ┴ └──┘
70 (λ hp2, begin
id └─┘
typ └─┘
st └─────
71 rw [euler_criterion hp this, neg_one_pow_eq_pow_mod_two, hp2, _root_.pow_zero,
id └─────────────┘ └┘ └──┘ └────────────────────────┘ └─┘ └─────────────┘
src └──┘└─────────────┘┴ ┴ └┘└────────────────────────┘└┘ └┘└─────────────┘└─
typ └──┘└─────────────┘┴└┘┴└──┘└┘└────────────────────────┘└┘└─┘└┘└─────────────┘└─
doc └──┘ ┴ ┴ └┘ └┘ └┘ └─
txt └──┘ ┴ ┴ └┘ └┘ └┘ └─
par └──┘ ┴ ┴ └┘ └┘ └┘ └─
pid └┘ ┴ ┴ └┘ └┘ └┘ └─
st ────────────────────────────────┘└──────────────────────────┘└───┘└───────────────┘└─
72 eq_self_iff_true, true_iff],
id └──────────────┘ └──────┘
src ───────┘└──────────────┘└┘└──────┘┴
typ ───────┘└──────────────┘└┘└──────┘┴
doc ───────┘ └┘ ┴
txt ───────┘ └┘ ┴
par ───────┘ └┘ ┴
pid ───────┘ └┘ ┴
st ───────────────────────┘└────────┘└──
73 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
74 rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl, h] at hp2,
id └────────────────────────┘ ┴ ┴ └─┘ ┴
src └────┘└────────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘ └──────┘
typ └────┘└────────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘┴└──────┘
doc └────┘ └┘ └─┘ └─┘ └───────┘ └┘ └──────┘
txt └────┘ └┘ └─┘ └─┘ └───────┘ └┘ └──────┘
par └────┘ └┘ └─┘ └─┘ └───────┘ └┘ └──────┘
pid └──┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴└─────┘
st ─────────────────────────────────────┘└────────────────────────┘└─┘┴└─────┘└─
75 exact absurd hp2 dec_trivial,
id └────┘ └─┘
src └────┘└────┘┴ ┴
typ └────┘└────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────┘└─
76 end)
st ──────┘
77 (λ hp2, begin
id └─┘
typ └─┘
st └─────
78 rw [euler_criterion hp this, neg_one_pow_eq_pow_mod_two, hp2, _root_.pow_one,
id └─────────────┘ └┘ └──┘ └────────────────────────┘ └─┘ └────────────┘
src └──┘└─────────────┘┴ ┴ └┘└────────────────────────┘└┘ └┘└────────────┘└─
typ └──┘└─────────────┘┴└┘┴└──┘└┘└────────────────────────┘└┘└─┘└┘└────────────┘└─
doc └──┘ ┴ ┴ └┘ └┘ └┘ └─
txt └──┘ ┴ ┴ └┘ └┘ └┘ └─
par └──┘ ┴ ┴ └┘ └┘ └┘ └─
pid └┘ ┴ ┴ └┘ └┘ └┘ └─
st ────────────────────────────────┘└──────────────────────────┘└───┘└──────────────┘└─
79 iff_false_intro (zmodp.ne_neg_self hp hp1 one_ne_zero).symm, false_iff,
id └─────────────┘ └───────────────┘ └┘ └─┘ └─────────┘ └───────┘
src ───────┘└─────────────┘┴ └───────────────┘┴ ┴ ┴└─────────┘└──────┘└───────┘└─
typ ───────┘└─────────────┘┴ └───────────────┘┴└┘┴└─┘┴└─────────┘└──────┘└───────┘└─
doc ───────┘ ┴ ┴ ┴ ┴ └──────┘ └─
txt ───────┘ ┴ ┴ ┴ ┴ └──────┘ └─
par ───────┘ ┴ ┴ ┴ ┴ └──────┘ └─
pid ───────┘ ┴ ┴ ┴ ┴ └──────┘ └─
st ─────────────────────────────────────────────────────────────────┘└──────────┘└─
80 not_not],
id └─────┘
src ───────┘└─────┘┴
typ ───────┘└─────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ──────────────┘└──
81 rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl] at hp2,
id └────────────────────────┘ └─┘
src └────┘└────────────────────────┘└┘ └─┘ └─┘ └───────┘└─┘└──────┘
typ └────┘└────────────────────────┘└┘ └─┘ └─┘ └───────┘└─┘└──────┘
doc └────┘ └┘ └─┘ └─┘ └───────┘ └──────┘
txt └────┘ └┘ └─┘ └─┘ └───────┘ └──────┘
par └────┘ └┘ └─┘ └─┘ └───────┘ └──────┘
pid └──┘ └┘ └─┘ └─┘ └───────┘ ┴└─────┘
st ─────────────────────────────────────┘└────────────────────────┘┴└─────┘└─
82 rw [← nat.mod_mul_left_mod _ 2, show 2 * 2 = 4, from rfl] at hp1,
id └──────────────────┘ └─┘
src └────┘└──────────────────┘└────┘ └─┘ └─┘ └───────┘└─┘└──────┘
typ └────┘└──────────────────┘└────┘ └─┘ └─┘ └───────┘└─┘└──────┘
doc └────┘ └────┘ └─┘ └─┘ └───────┘ └──────┘
txt └────┘ └────┘ └─┘ └─┘ └───────┘ └──────┘
par └────┘ └────┘ └─┘ └─┘ └───────┘ └──────┘
pid └──┘ └────┘ └─┘ └─┘ └───────┘ ┴└─────┘
st ──────────────────────────────────┘└─────────────────────────┘┴└─────┘└─
83 have hp4 : p % 4 < 4, from nat.mod_lt _ dec_trivial,
id ┴ ┴ ┴ └────────┘
src └─────────┘ ┴┴└─┘┴└┘ └───┘└────────┘└─┘
typ └─────────┘┴┴┴└─┘┴└┘ └───┘└────────┘└─┘
doc └─────────┘ ┴ └─┘ └┘ └───┘ └─┘
txt └─────────┘ ┴ └─┘ └┘ └───┘ └─┘
par └─────────┘ ┴ └─┘ └┘ └───┘ └─┘
pid └──────┘└─┘ ┴ └─┘ ┴┴ └───┘ └─┘
st ─────────────────────────┘└─────────────────────────────┘└─
84 revert hp1 hp2, revert hp4,
src └────────────┘ └────────┘
typ └────────────┘ └────────┘
doc └────────────┘ └────────┘
txt └────────────┘ └────────┘
par └────────────┘ └────────┘
pid └──────┘ └──┘
st ───────────────────┘└──────────┘└─
85 generalize : p % 4 = k,
id ┴
src └───────────┘ ┴ └─┘ ┴
typ └───────────┘┴┴ └─┘ ┴
doc └───────────┘ ┴ └─┘ ┴
txt └───────────┘ ┴ └─┘ ┴
par └───────────┘ ┴ └─┘ ┴
pid ┴┴┴ ┴ └─┘ ┴
st ───────────────────────────┘└─
86 revert k, exact dec_trivial
src └──────┘ └────┘ └
typ └──────┘ └────┘ └
doc └──────┘ └────┘ └
txt └──────┘ └────┘ └
par └──────┘ └────┘ └
pid └┘ ┴ └
st ─────────────┘└───────────────────
87 end))
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
88
89 lemma pow_div_two_eq_neg_one_or_one {a : zmodp p hp} (ha : a ≠ 0) : a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1 :=
id └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
90 hp.eq_two_or_odd.elim
id └┘└────────────┘└───┘
src └────────────┘└───┘
typ └┘└────────────┘└───┘
91 (λ h, by revert a ha; resetI; subst h; exact dec_trivial)
id ┴ ┴ └─────────┘
src └─────────┘ └────┘ └────┘ └────┘└─────────┘
typ ┴ └─────────┘ └────┘ └────┘┴ └────┘└─────────┘
doc └─────────┘ └────┘ └────┘ └────┘└─────────┘
txt └─────────┘ └────┘ └────┘ └────┘
par └─────────┘ └────┘ └────┘ └────┘
pid └───┘ ┴ ┴
st └──────────────────────────────────────────────┘
92 (λ hp1, by rw [← mul_self_eq_one_iff, ← _root_.pow_add, ← two_mul, two_mul_odd_div_two hp1];
id └─┘ └─────────────────┘ └────────────┘ └─────┘ └─────────────────┘ └─┘
src └────┘└─────────────────┘└──┘└────────────┘└──┘└─────┘└┘└─────────────────┘┴ ┴
typ └─┘ └────┘└─────────────────┘└──┘└────────────┘└──┘└─────┘└┘└─────────────────┘┴└─┘┴
doc └────┘ └──┘ └──┘ └┘ ┴ ┴
txt └────┘ └──┘ └──┘ └┘ ┴ ┴
par └────┘ └──┘ └──┘ └┘ ┴ ┴
pid └──┘ └──┘ └──┘ └┘ ┴ ┴
st └────────────────────────┘└────────────────┘└─────────┘└───────────────────────┘┴└─
93 exact fermat_little hp ha)
id └───────────┘ └┘ └┘
src └────┘└───────────┘┴ ┴
typ └────┘└───────────┘┴└┘┴└┘
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────┘
94
95 @[simp] lemma wilsons_lemma {p : ℕ} (hp : nat.prime p) : (fact (p - 1) : zmodp p hp) = -1 :=
id ┴ └───────┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
src ┴ └───────┘ └──┘ ┴ └───┘ ┴ ┴
typ ┴ └───────┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
doc └──┘ └───────┘ └──┘
96 begin
st └─────
97 rw [← finset.prod_Ico_id_eq_fact, ← @units.coe_one (zmodp p hp), ← units.coe_neg,
id └────────────────────────┘ └───────────┘ └───┘ ┴ └┘ └───────────┘
src └────┘└────────────────────────┘└──┘ └───────────┘┴ └───┘┴ ┴ └───┘└───────────┘└─
typ └────┘└────────────────────────┘└──┘ └───────────┘┴ └───┘┴┴┴└┘└───┘└───────────┘└─
doc └────┘ └──┘ ┴ ┴ ┴ └───┘└───────────┘└─
txt └────┘ └──┘ ┴ ┴ ┴ └───┘ └─
par └────┘ └──┘ ┴ ┴ ┴ └───┘ └─
pid └──┘ └──┘ ┴ ┴ ┴ └───┘ └─
st ─────────────────────────────────┘└─────────────────────────────┘└───────────────┘└─
98 ← @prod_univ_units_id_eq_neg_one (zmodp p hp),
id └───────────────────────────┘ └───┘ ┴ └┘
src ─────┘ └───────────────────────────┘┴ └───┘┴ ┴ └──
typ ─────┘ └───────────────────────────┘┴ └───┘┴┴┴└┘└──
doc ─────┘ ┴ ┴ ┴ └──
txt ─────┘ ┴ ┴ ┴ └──
par ─────┘ ┴ ┴ ┴ └──
pid ─────┘ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────┘└─
99 ← prod_hom _ (coe : units (zmodp p hp) → zmodp p hp),
id └──────┘ └─┘ └───┘ └───┘ ┴ └┘
src ─────┘└──────┘└─┘ └─┘└─┘└───┘┴ ┴ ┴ └┘ ┴└───┘┴ ┴ └──
typ ─────┘└──────┘└─┘ └─┘└─┘└───┘┴ ┴ ┴ └┘ ┴└───┘┴┴┴└┘└──
doc ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
txt ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────────┘└─
100 ← prod_hom _ (coe : ℕ → zmodp p hp)],
id └──────┘ └─┘ └───┘ ┴ └┘
src ─────┘└──────┘└─┘ └─┘└─┘ ┴ ┴└───┘┴ ┴ └┘
typ ─────┘└──────┘└─┘ └─┘└─┘ ┴ ┴└───┘┴┴┴└┘└┘
doc ─────┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘
txt ─────┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘
par ─────┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘
pid ─────┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────┘└──
101 exact eq.symm (prod_bij
id └─────┘ └──────┘
src └────┘└─────┘┴ └──────┘└
typ └────┘└─────┘┴ └──────┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ──────────────────────────
102 (λ a _, (a : zmodp p hp).1)
src ───┘ └────┘ └─┘ ┴ ┴ └────
typ ───┘ └────┘ └─┘ ┴ ┴ └────
doc ───┘ └────┘ └─┘ ┴ ┴ └────
txt ───┘ └────┘ └─┘ ┴ ┴ └────
par ───┘ └────┘ └─┘ ┴ ┴ └────
pid ───┘ └────┘ └─┘ ┴ ┴ └────
st ────────────────────────────────
103 (λ a ha, Ico.mem.2 ⟨nat.pos_of_ne_zero
id └─────┘ └────────────────┘
src ───┘ └─────┘└─────┘└─┘ └────────────────┘└
typ ───┘ └─────┘└─────┘└─┘ └────────────────┘└
doc ───┘ └─────┘ └─┘ └
txt ───┘ └─────┘ └─┘ └
par ───┘ └─────┘ └─┘ └
pid ───┘ └─────┘ └─┘ └
st ───────────────────────────────────────────
104 (λ h, units.coe_ne_zero a (fin.eq_of_veq h)),
id └───────────────┘
src ───────┘ └──┘└───────────────┘┴ ┴ ┴ └───
typ ───────┘ └──┘└───────────────┘┴ ┴ ┴ └───
doc ───────┘ └──┘└───────────────┘┴ ┴ ┴ └───
txt ───────┘ └──┘ ┴ ┴ ┴ └───
par ───────┘ └──┘ ┴ ┴ ┴ └───
pid ───────┘ └──┘ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────
105 by rw [← succ_sub hp.pos, succ_sub_one]; exact (a : zmodp p hp).2⟩)
id └──────┘ └────┘ └──────────┘ ┴ └───┘ ┴ └┘
src ─────┘ ┴└────┘└──────┘┴└────┘└┘└──────────┘┴└──────┘ └─┘└───┘┴ ┴ └─────
typ ─────┘ ┴└────┘└──────┘┴└────┘└┘└──────────┘┴└──────┘ ┴└─┘└───┘┴┴┴└┘└─────
doc ─────┘ ┴└────┘ ┴ └┘ ┴└──────┘ └─┘ ┴ ┴ └─────
txt ─────┘ ┴└────┘ ┴ └┘ ┴└──────┘ └─┘ ┴ ┴ └─────
par ─────┘ ┴└────┘ ┴ └┘ ┴└──────┘ └─┘ ┴ ┴ └─────
pid ─────┘ └─────┘ ┴ └┘ └───────┘ └─┘ ┴ ┴ └─────
st ───────┘└────────────────────┘└────────────┘┴└────────────────────────┘└──
106 (λ a _, by simp) (λ _ _ _ _, units.ext_iff.2 ∘ fin.eq_of_veq)
id └───────────┘ ┴ └───────────┘
src ───┘ └────┘ ┴└──┘└┘ └────────┘└───────────┘└─┘┴┴└───────────┘└─
typ ───┘ └────┘ ┴└──┘└┘ └────────┘└───────────┘└─┘┴┴└───────────┘└─
doc ───┘ └────┘ ┴└──┘└┘ └────────┘ └─┘ ┴ └─
txt ───┘ └────┘ ┴└──┘└┘ └────────┘ └─┘ ┴ └─
par ───┘ └────┘ ┴└──┘└┘ └────────┘ └─┘ ┴ └─
pid ───┘ └────┘ └─────┘ └────────┘ └─┘ ┴ └─
st ─────────────┘└───┘└──────────────────────────────────────────────
107 (λ b hb,
src ───┘ └──────
typ ───┘ └──────
doc ───┘ └──────
txt ───┘ └──────
par ───┘ └──────
pid ───┘ └──────
st ─────────────
108 have b ≠ 0 ∧ b < p, by rwa [Ico.mem, nat.succ_le_iff, ← succ_sub hp.pos,
id ┴ ┴ ┴ └─────┘ └─────────────┘ └──────┘ └────┘
src ─────┘ └─┘┴└─┘┴┴ ┴┴┴ └───┘└───┘└─────┘└┘└─────────────┘└──┘└──────┘┴└────┘└─
typ ─────┘ └─┘┴└─┘┴┴ ┴┴┴ └───┘└───┘└─────┘└┘└─────────────┘└──┘└──────┘┴└────┘└─
doc ─────┘ └─┘ └─┘ ┴ ┴ ┴ └───┘└───┘ └┘ └──┘ ┴ └─
txt ─────┘ └─┘ └─┘ ┴ ┴ ┴ └───┘└───┘ └┘ └──┘ ┴ └─
par ─────┘ └─┘ └─┘ ┴ ┴ ┴ └───┘└───┘ └┘ └──┘ ┴ └─
pid ─────┘ └─┘ └─┘ ┴ ┴ ┴ └────────┘ └┘ └──┘ ┴ └─
st ───────────────────────────┘└───────────┘└───────────────┘└─────────────────┘└─
109 succ_sub_one, nat.pos_iff_ne_zero] at hb,
id └──────────┘ └─────────────────┘
src ───────┘└──────────┘└┘└─────────────────┘└─────┘└─
typ ───────┘└──────────┘└┘└─────────────────┘└─────┘└─
doc ───────┘ └┘ └─────┘└─
txt ───────┘ └┘ └─────┘└─
par ───────┘ └┘ └─────┘└─
pid ───────┘ └┘ └────────
st ───────────────────┘└───────────────────┘┴└────┘└─
110 ⟨units.mk0 _ (show (b : zmodp p hp) ≠ 0, from fin.ne_of_vne $
id └───────┘ └───┘ ┴ └┘ ┴ └───────────┘
src ─────┘ └───────┘└─┘ ┴ └─┘└───┘┴ ┴ └┘ └───────┘└───────────┘┴ └
typ ─────┘ └───────┘└─┘ ┴ └─┘└───┘┴┴┴└┘└┘┴└───────┘└───────────┘┴ └
doc ─────┘ └───────┘└─┘ ┴ └─┘ ┴ ┴ └┘ └───────┘ ┴ └
txt ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘ └───────┘ ┴ └
par ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘ └───────┘ ┴ └
pid ─────┘ └─┘ ┴ └─┘ ┴ ┴ └┘ └───────┘ ┴ └
st ────────────────────────────────────────────────────────────────────
111 by rw [zmod.val_cast_nat, ← @nat.cast_zero (zmodp p hp), zmod.val_cast_nat];
id └───────────────┘ └───────────┘ └───┘ ┴ └┘ └───────────────┘
src ───────┘ ┴└──┘└───────────────┘└──┘ └───────────┘┴ └───┘┴ ┴ └─┘└───────────────┘┴└─
typ ───────┘ ┴└──┘└───────────────┘└──┘ └───────────┘┴ └───┘┴┴┴└┘└─┘└───────────────┘┴└─
doc ───────┘ ┴└──┘ └──┘ ┴ ┴ ┴ └─┘ ┴└─
txt ───────┘ ┴└──┘ └──┘ ┴ ┴ ┴ └─┘ ┴└─
par ───────┘ ┴└──┘ └──┘ ┴ ┴ ┴ └─┘ ┴└─
pid ───────┘ └───┘ └──┘ ┴ ┴ ┴ └─┘ └──
st ─────────┘└────────────────────┘└─────────────────────────────┘└─────────────────┘┴└─
112 simp [mod_eq_of_lt this.2, this.1]), mem_univ _,
id └──────────┘ └──┘ └──┘ └──────┘
src ───────┘└────┘└──────────┘┴ └──┘ └─┘└─┘└──────┘└───
typ ───────┘└────┘└──────────┘┴└──┘└──┘└──┘└─┘└─┘└──────┘└───
doc ───────┘└────┘ ┴ └──┘ └─┘└─┘ └───
txt ───────┘└────┘ ┴ └──┘ └─┘└─┘ └───
par ───────┘└────┘ ┴ └──┘ └─┘└─┘ └───
pid ─────────────┘ ┴ └──┘ └────┘ └───
st ─────────────────────────────────────────┘└──────────────
113 by simp [val_cast_of_lt hp this.2]⟩))
id └────────────┘ └┘ └──┘
src ─────┘ ┴└────┘└────────────┘┴ ┴ └─┘└──┘
typ ─────┘ ┴└────┘└────────────┘┴└┘┴└──┘└─┘└──┘
doc ─────┘ ┴└────┘ ┴ ┴ └─┘└──┘
txt ─────┘ ┴└────┘ ┴ ┴ └─┘└──┘
par ─────┘ ┴└────┘ ┴ ┴ └─┘└──┘
pid ─────┘ └─────┘ ┴ ┴ └────┘┴
st ───────┘└──────────────────────────────┘└──┘
114 end
st └─┘
115
116 @[simp] lemma prod_Ico_one_prime {p : ℕ} (hp : nat.prime p) :
id ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ └───────┘ ┴
doc └──┘ └───────┘
117 (Ico 1 p).prod (λ x, (x : zmodp p hp)) = -1 :=
id └─┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
src └─┘ └──┘ └───┘ ┴ ┴
typ └─┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
doc └─┘ └──┘
118 by conv in (Ico 1 p) { rw [← succ_sub_one p, succ_sub hp.pos] };
id └─┘ ┴ └──────────┘ ┴ └──────┘ └────┘
src └──────┘ └─┘└─┘ └──┘└────┘└──────────┘┴ └┘└──────┘┴└────┘└┘┴
typ └──────┘ └─┘└─┘┴└──┘└────┘└──────────┘┴┴└┘└──────┘┴└────┘└┘┴
doc └─┘
txt └──────┘ └─┘ └──┘└────┘ ┴ └┘ ┴ └┘┴
par └──────┘ └─┘ └──┘└────┘ ┴ └┘ ┴ └┘┴
pid ┴└─┘ └─┘ ┴└───────┘ ┴ └┘ ┴ └─┘
st └──────────────────┘└───────────────────┘└───────────────┘ ┴└┘└
119 rw [prod_hom _ (coe : ℕ → zmodp p hp),
id └──────┘ └─┘ └───┘ ┴ └┘
src └──┘└──────┘└─┘ └─┘└─┘ ┴ ┴└───┘┴ ┴ └──
typ └──┘└──────┘└─┘ └─┘└─┘ ┴ ┴└───┘┴┴┴└┘└──
doc └──┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └──
txt └──┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └──
par └──┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └──
pid └┘ └─┘ └─┘ ┴ ┴ ┴ ┴ └──
st ─────┘└───────────────────────────────┘└─
120 finset.prod_Ico_id_eq_fact, wilsons_lemma]
id └────────────────────────┘ └───────────┘
src ───┘└────────────────────────┘└┘└───────────┘└─
typ ───┘└────────────────────────┘└┘└───────────┘└─
doc ───┘ └┘ └─
txt ───┘ └┘ └─
par ───┘ └┘ └─
pid ───┘ └┘ ┴└
st ─────────────────────────────┘└─────────────┘┴└
121
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
122 end zmodp
123
124 /-- The image of the map sending a non zero natural number `x ≤ p / 2` to the absolute value
125 of the element of interger in the interval `(-p/2, p/2]` congruent to `a * x` mod p is the set
126 of non zero natural numbers `x` such that `x ≤ p / 2` -/
127 lemma Ico_map_val_min_abs_nat_abs_eq_Ico_map_id
128 {p : ℕ} (hp : p.prime) (a : zmodp p hp) (hpa : a ≠ 0) :
id ┴ ┴└────┘ └───┘ ┴ └┘ ┴ ┴
src ┴ └────┘ └───┘ ┴
typ ┴ ┴└────┘ └───┘ ┴ └┘ ┴ ┴
doc └────┘
129 (Ico 1 (p / 2).succ).1.map (λ x, (a * x).val_min_abs.nat_abs) =
id └─┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─────────┘ └─────┘ ┴
src └─┘ ┴ └──┘ ┴ └─┘ ┴ └─────────┘ └─────┘ ┴
typ └─┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─────────┘ └─────┘ ┴
doc └─┘ └─┘ └─────────┘
130 (Ico 1 (p / 2).succ).1.map (λ a, a) :=
id └─┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴
src └─┘ ┴ └──┘ ┴ └─┘
typ └─┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴
doc └─┘ └─┘
131 have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2,
id ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
132 by simp [nat.lt_succ_iff, nat.succ_le_iff, nat.pos_iff_ne_zero] {contextual := tt},
id └─────────────┘ └─────────────┘ └─────────────────┘ └┘
src └────┘└─────────────┘└┘└─────────────┘└┘└─────────────────┘└┘ └────────────┘└┘┴
typ └────┘└─────────────┘└┘└─────────────┘└┘└─────────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ └┘ ┴┴ └────────────┘ ┴
st └──────────────────────────────────────────────────────────────────────────────┘
133 have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p,
id ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └─┘ ┴ └──┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └─┘
134 from λ x hx, lt_of_le_of_lt (he hx).2 (nat.div_lt_self hp.pos dec_trivial),
id ┴ └┘ └────────────┘ └┘ └┘ ┴ └─────────────┘ └┘└──┘ └─────────┘
src └────────────┘ ┴ └─────────────┘ └──┘ └─────────┘
typ ┴ └┘ └────────────┘ └┘ └┘ ┴ └─────────────┘ └┘└──┘ └─────────┘
doc └─────────┘
135 have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬ p ∣ x,
id ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └─┘
136 from λ x hx hpx, not_lt_of_ge (le_of_dvd (nat.pos_of_ne_zero (he hx).1) hpx) (hep hx),
id ┴ └┘ └─┘ └──────────┘ └───────┘ └────────────────┘ └┘ └┘ ┴ └─┘ └─┘ └┘
src └──────────┘ └───────┘ └────────────────┘ ┴
typ ┴ └┘ └─┘ └──────────┘ └───────┘ └────────────────┘ └┘ └┘ ┴ └─┘ └─┘ └┘
137 have hsurj : ∀ b : ℕ , b ∈ Ico 1 (p / 2).succ →
id ┴ ┴ ┴ └─┘ ┴ ┴ └──┘
src ┴ ┴ └─┘ ┴ └──┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘
doc └─┘
138 ∃ x ∈ Ico 1 (p / 2).succ,
id ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
src ┴ └─┘ ┴ └──┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
doc └─┘
139 b = (a * x : zmodp p hp).val_min_abs.nat_abs,
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
src ┴ ┴ └───┘ └─────────┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
doc └─────────┘
140 from λ b hb, ⟨(b / a : zmodp p hp).val_min_abs.nat_abs,
id ┴ └┘ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
src ┴ └───┘ └─────────┘ └─────┘
typ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
doc └─────────┘
141 Ico.mem.2 ⟨nat.pos_of_ne_zero $
id └─────┘┴ └────────────────┘
src └─────┘┴ └────────────────┘
typ └─────┘┴ └────────────────┘
142 by simp [div_eq_mul_inv, hpa, zmodp.eq_zero_iff_dvd_nat hp b, hpe hb],
id └────────────┘ └─┘ └───────────────────────┘ └┘ ┴ └─┘ └┘
src └────┘└────────────┘└┘ └┘└───────────────────────┘┴ ┴ └┘ ┴ ┴
typ └────┘└────────────┘└┘└─┘└┘└───────────────────────┘┴└┘┴┴└┘└─┘┴└┘┴
doc └────┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴
txt └────┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴
par └────┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴
pid ┴┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴
st └─────────────────────────────────────────────────────────────────┘
143 nat.lt_succ_of_le $ zmodp.nat_abs_val_min_abs_le _⟩,
id └───────────────┘ └──────────────────────────┘
src └───────────────┘ └──────────────────────────┘
typ └───────────────┘ └──────────────────────────┘
144 begin
st └─────
145 rw [zmodp.cast_nat_abs_val_min_abs],
id └────────────────────────────┘
src └──┘└────────────────────────────┘┴
typ └──┘└────────────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────────────────────────────┘└──
146 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────────┘└─
147 { erw [mul_div_cancel' _ hpa, zmodp.val_min_abs, zmod.val_min_abs,
id └─────────────┘ └─┘ └───────────────┘ └──────────────┘
src └───┘└─────────────┘└─┘ └┘└───────────────┘└┘└──────────────┘└─
typ └───┘└─────────────┘└─┘└─┘└┘└───────────────┘└┘└──────────────┘└─
doc └───┘ └─┘ └┘└───────────────┘└┘└──────────────┘└─
txt └───┘ └─┘ └┘ └┘ └─
par └───┘ └─┘ └┘ └┘ └─
pid └┘ └─┘ └┘ └┘ └─
st ───────┘└────────────────────────┘└─────────────────┘└────────────────┘└─
148 zmodp.val_cast_of_lt hp (hep hb), if_pos (le_of_lt_succ (Ico.mem.1 hb).2),
id └──────────────────┘ └┘ └─┘ └┘ └────┘ └───────────┘ └─────┘ └┘
src ─────────┘└──────────────────┘┴ ┴ ┴ └─┘└────┘┴ └───────────┘┴ └─────┘└─┘ └─────
typ ─────────┘└──────────────────┘┴└┘┴ └─┘┴└┘└─┘└────┘┴ └───────────┘┴ └─────┘└─┘└┘└─────
doc ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─────
txt ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─────
par ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─────
pid ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─────
st ─────────────────────────────────────────┘└───────────────────────────────────────┘└─
149 int.nat_abs_of_nat], },
id └────────────────┘
src ─────────┘└────────────────┘┴
typ ─────────┘└────────────────┘┴
doc ─────────┘ ┴
txt ─────────┘ ┴
par ─────────┘ ┴
pid ─────────┘ ┴
st ───────────────────────────┘└───┘└
150 { erw [mul_neg_eq_neg_mul_symm, mul_div_cancel' _ hpa, zmod.nat_abs_val_min_abs_neg,
id └─────────────────────┘ └─────────────┘ └─┘ └──────────────────────────┘
src └───┘└─────────────────────┘└┘└─────────────┘└─┘ └┘└──────────────────────────┘└─
typ └───┘└─────────────────────┘└┘└─────────────┘└─┘└─┘└┘└──────────────────────────┘└─
doc └───┘ └┘ └─┘ └┘ └─
txt └───┘ └┘ └─┘ └┘ └─
par └───┘ └┘ └─┘ └┘ └─
pid └┘ └┘ └─┘ └┘ └─
st ───────────────────────────────────┘└─────────────────────┘└────────────────────────────┘└─
151 zmod.val_min_abs, zmodp.val_cast_of_lt hp (hep hb),
id └──────────────┘ └──────────────────┘ └┘ └─┘ └┘
src ─────────┘└──────────────┘└┘└──────────────────┘┴ ┴ ┴ └──
typ ─────────┘└──────────────┘└┘└──────────────────┘┴└┘┴ └─┘┴└┘└──
doc ─────────┘└──────────────┘└┘ ┴ ┴ ┴ └──
txt ─────────┘ └┘ ┴ ┴ ┴ └──
par ─────────┘ └┘ ┴ ┴ ┴ └──
pid ─────────┘ └┘ ┴ ┴ ┴ └──
st ─────────────────────────┘└────────────────────────────────┘└─
152 if_pos (le_of_lt_succ (Ico.mem.1 hb).2), int.nat_abs_of_nat] },
id └────┘ └───────────┘ └─────┘ └┘ └────────────────┘
src ─────────┘└────┘┴ └───────────┘┴ └─────┘└─┘ └────┘└────────────────┘└┘
typ ─────────┘└────┘┴ └───────────┘┴ └─────┘└─┘└┘└────┘└────────────────┘└┘
doc ─────────┘ ┴ ┴ └─┘ └────┘ └┘
txt ─────────┘ ┴ ┴ └─┘ └────┘ └┘
par ─────────┘ ┴ ┴ └─┘ └────┘ └┘
pid ─────────┘ ┴ ┴ └─┘ └────┘ ┴┴
st ────────────────────────────────────────────────┘└──────────────────┘┴┴└──
153 end⟩,
st ──────┘
154 have hmem : ∀ x : ℕ, x ∈ Ico 1 (p / 2).succ →
id ┴ ┴ ┴ └─┘ ┴ ┴ └──┘
src ┴ ┴ └─┘ ┴ └──┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘
doc └─┘
155 (a * x : zmodp p hp).val_min_abs.nat_abs ∈ Ico 1 (p / 2).succ,
id ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ ┴ └─┘ ┴ ┴ └──┘
src ┴ └───┘ └─────────┘ └─────┘ ┴ └─┘ ┴ └──┘
typ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ ┴ └─┘ ┴ ┴ └──┘
doc └─────────┘ └─┘
156 from λ x hx, by simp [hpa, zmodp.eq_zero_iff_dvd_nat hp x, hpe hx, lt_succ_iff, succ_le_iff,
id ┴ └┘ └─┘ └───────────────────────┘ └┘ ┴ └─┘ └┘ └─────────┘ └─────────┘
src └────┘ └┘└───────────────────────┘┴ ┴ └┘ ┴ └┘└─────────┘└┘└─────────┘└─
typ ┴ └┘ └────┘└─┘└┘└───────────────────────┘┴└┘┴┴└┘└─┘┴└┘└┘└─────────┘└┘└─────────┘└─
doc └────┘ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─
txt └────┘ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─
par └────┘ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─
pid ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─
st └─────────────────────────────────────────────────────────────────────────────
157 nat.pos_iff_ne_zero, zmodp.nat_abs_val_min_abs_le _],
id └─────────────────┘ └──────────────────────────┘
src ───────┘└─────────────────┘└┘└──────────────────────────┘└─┘
typ ───────┘└─────────────────┘└┘└──────────────────────────┘└─┘
doc ───────┘ └┘ └─┘
txt ───────┘ └┘ └─┘
par ───────┘ └┘ └─┘
pid ───────┘ └┘ └─┘
st ───────────────────────────────────────────────────────────┘
158 multiset.map_eq_map_of_bij_of_nodup _ _ (finset.nodup _) (finset.nodup _)
id └─────────────────────────────────┘ └──────────┘ └──────────┘
src └─────────────────────────────────┘ └──────────┘ └──────────┘
typ └─────────────────────────────────┘ └──────────┘ └──────────┘
159 (λ x _, (a * x : zmodp p hp).val_min_abs.nat_abs) hmem (λ _ _, rfl)
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘
src ┴ └───┘ └─────────┘ └─────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘
doc └─────────┘
160 (inj_on_of_surj_on_of_card_le _ hmem hsurj (le_refl _)) hsurj
id └──────────────────────────┘ └──┘ └───┘ └─────┘ └───┘
src └──────────────────────────┘ └─────┘
typ └──────────────────────────┘ └──┘ └───┘ └─────┘ └───┘
161
162 private lemma gauss_lemma_aux₁ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id ┴ ┴└────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴
typ ┴ ┴└────┘ ┴ ┴ ┴ ┴
doc └────┘
163 (hpa : (a : zmodp p hp) ≠ 0) :
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
164 (a^(p / 2) * (p / 2).fact : zmodp p hp) =
id ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ └──┘ └───┘ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ └┘ ┴
doc └──┘
165 (-1)^((Ico 1 (p / 2).succ).filter
id ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src ┴ ┴ └─┘ ┴ └──┘ └────┘
typ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
166 (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card * (p / 2).fact :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
167 calc (a ^ (p / 2) * (p / 2).fact : zmodp p hp) =
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ └┘
src ┴ ┴ ┴ ┴ └──┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ └┘
doc └──┘
168 (Ico 1 (p / 2).succ).prod (λ x, a * x) :
id └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └──┘ ┴
typ └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
doc └─┘ └──┘
169 by rw [prod_mul_distrib, ← prod_nat_cast, ← prod_nat_cast, prod_Ico_id_eq_fact,
id └──────────────┘ └───────────┘ └───────────┘ └─────────────────┘
src └──┘└──────────────┘└──┘└───────────┘└──┘└───────────┘└┘└─────────────────┘└─
typ └──┘└──────────────┘└──┘└───────────┘└──┘└───────────┘└┘└─────────────────┘└─
doc └──┘ └──┘ └──┘ └┘ └─
txt └──┘ └──┘ └──┘ └┘ └─
par └──┘ └──┘ └──┘ └┘ └─
pid └┘ └──┘ └──┘ └┘ └─
st └───────────────────┘└───────────────┘└───────────────┘└───────────────────┘└─
170 prod_const, Ico.card, succ_sub_one]; simp
id └────────┘ └──────┘ └──────────┘
src ─────┘└────────┘└┘└──────┘└┘└──────────┘┴ └───┘
typ ─────┘└────────┘└┘└──────┘└┘└──────────┘┴ └───┘
doc ─────┘ └┘ └┘ ┴ └───┘
txt ─────┘ └┘ └┘ ┴ └───┘
par ─────┘ └┘ └┘ ┴ └───┘
pid ─────┘ └┘ └┘ ┴ ┴
st ───────────────┘└────────┘└────────────┘┴└─────┘
171 ... = (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmodp p hp).val) : by simp
id └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘
src └─┘ ┴ └──┘ └──┘ ┴ └───┘ └─┘ └───┘
typ └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └───┘
doc └─┘ └──┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
172 ... = (Ico 1 (p / 2).succ).prod
id └─┘ ┴ ┴ └──┘ └──┘
src └─┘ ┴ └──┘ └──┘
typ └─┘ ┴ ┴ └──┘ └──┘
doc └─┘ └──┘
173 (λ x, (if (a * x : zmodp p hp).val ≤ p / 2 then 1 else -1) *
id ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴
174 (a * x : zmodp p hp).val_min_abs.nat_abs) :
id ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
src ┴ └───┘ └─────────┘ └─────┘
typ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
doc └─────────┘
175 prod_congr rfl $ λ _ _, begin
id └────────┘ └─┘ ┴ ┴
src └────────┘ └─┘
typ └────────┘ └─┘ ┴ ┴
st └─────
176 simp only [zmodp.cast_nat_abs_val_min_abs],
id └────────────────────────────┘
src └─────────┘└────────────────────────────┘┴
typ └─────────┘└────────────────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────────────────────────┘└─
177 split_ifs; simp
src └───────┘ └────
typ └───────┘ └────
doc └───────┘ └────
txt └───────┘ └────
par └───────┘ └────
pid └
st ────────────────────
178 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
179 ... = (-1)^((Ico 1 (p / 2).succ).filter
id ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src ┴ ┴ └─┘ ┴ └──┘ └────┘
typ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
180 (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card *
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘
181 (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmodp p hp).val_min_abs.nat_abs) :
id └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
src └─┘ ┴ └──┘ └──┘ ┴ └───┘ └─────────┘ └─────┘
typ └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘
doc └─┘ └──┘ └─────────┘
182 have (Ico 1 (p / 2).succ).prod
id └─┘ ┴ ┴ └──┘ └──┘
src └─┘ ┴ └──┘ └──┘
typ └─┘ ┴ ┴ └──┘ └──┘
doc └─┘ └──┘
183 (λ x, if (a * x : zmodp p hp).val ≤ p / 2 then (1 : zmodp p hp) else -1) =
id ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
src ┴ └───┘ └─┘ ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
184 ((Ico 1 (p / 2).succ).filter
id └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
185 (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).prod (λ _, -1),
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
186 from prod_bij_ne_one (λ x _ _, x)
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴
187 (λ x, by split_ifs; simp * at * {contextual := tt})
id ┴ └┘
src └───────┘ └──────────┘ └────────────┘└┘┴
typ ┴ └───────┘ └──────────┘ └────────────┘└┘┴
doc └───────┘ └──────────┘ └────────────┘ ┴
txt └───────┘ └──────────┘ └────────────┘ ┴
par └───────┘ └──────────┘ └────────────┘ ┴
pid ┴┴┴└──┘┴ └────────────┘ ┴
st └────────────────────────────────────────┘
188 (λ _ _ _ _ _ _, id)
id ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘
189 (λ b h _, ⟨b, by simp [-not_le, *] at *⟩)
id ┴ ┴ ┴ ┴
src └────────────────────┘
typ ┴ ┴ ┴ ┴ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid ┴└──────────┘┴└──┘
st └─────────────────────┘
190 (by intros; split_ifs at *; simp * at *),
src └────┘ └────────────┘ └─────────┘
typ └────┘ └────────────┘ └─────────┘
doc └────┘ └────────────┘ └─────────┘
txt └────┘ └────────────┘ └─────────┘
par └────┘ └────────────┘ └─────────┘
pid └───┘ ┴┴┴└──┘
st └──────────────────────────────────┘
191 by rw [prod_mul_distrib, this]; simp
id └──────────────┘ └──┘
src └──┘└──────────────┘└┘ ┴ └───┘
typ └──┘└──────────────┘└┘└──┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st └───────────────────┘└────┘┴└─────┘
192 ... = (-1)^((Ico 1 (p / 2).succ).filter
id ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src ┴ ┴ └─┘ ┴ └──┘ └────┘
typ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
193 (λ x : ℕ, ¬(a * x : zmodp p hp).val ≤ p / 2)).card * (p / 2).fact :
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
194 by rw [← prod_nat_cast, finset.prod_eq_multiset_prod,
id └───────────┘ └──────────────────────────┘
src └────┘└───────────┘└┘└──────────────────────────┘└─
typ └────┘└───────────┘└┘└──────────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st └──────────────────┘└────────────────────────────┘└─
195 Ico_map_val_min_abs_nat_abs_eq_Ico_map_id hp a hpa,
id └───────────────────────────────────────┘ └┘ ┴ └─┘
src ─────┘└───────────────────────────────────────┘┴ ┴ ┴ └─
typ ─────┘└───────────────────────────────────────┘┴└┘┴┴┴└─┘└─
doc ─────┘└───────────────────────────────────────┘┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────────────┘└─
196 ← finset.prod_eq_multiset_prod, prod_Ico_id_eq_fact]
id └──────────────────────────┘ └─────────────────┘
src ───────┘└──────────────────────────┘└┘└─────────────────┘└─
typ ───────┘└──────────────────────────┘└┘└─────────────────┘└─
doc ───────┘ └┘ └─
txt ───────┘ └┘ └─
par ───────┘ └┘ └─
pid ───────┘ └┘ ┴└
st ───────────────────────────────────┘└───────────────────┘┴└
197
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
198 private lemma gauss_lemma_aux₂ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id ┴ ┴└────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴
typ ┴ ┴└────┘ ┴ ┴ ┴ ┴
doc └────┘
199 (hpa : (a : zmodp p hp) ≠ 0) :
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
200 (a^(p / 2) : zmodp p hp) = (-1)^((Ico 1 (p / 2).succ).filter
id ┴┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └────┘
typ ┴┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
201 (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
doc └──┘
202 (domain.mul_right_inj
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
203 (show ((p / 2).fact : zmodp p hp) ≠ 0,
id ┴ ┴ └──┘ └───┘ ┴ └┘ ┴
src ┴ └──┘ └───┘ ┴
typ ┴ ┴ └──┘ └───┘ ┴ └┘ ┴
doc └──┘
204 by rw [ne.def, zmodp.eq_zero_iff_dvd_nat, hp.dvd_fact, not_le];
id └────┘ └───────────────────────┘ └────┘
src └──┘└────┘└┘└───────────────────────┘└┘ └┘└────┘┴
typ └──┘└────┘└┘└───────────────────────┘└┘└─────────┘└┘└────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────────┘└─────────────────────────┘└───────────┘└──────┘┴└─
205 exact nat.div_lt_self hp.pos dec_trivial)).1 $
id └─────────────┘ └────┘ └─────────┘ ┴
src └────┘└─────────────┘┴└────┘┴└─────────┘ ┴
typ └────┘└─────────────┘┴└────┘┴└─────────┘ ┴
doc └────┘ ┴ ┴└─────────┘
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────────────────────┘
206 by simpa using gauss_lemma_aux₁ _ hp2 hpa
id └──────────────┘ └─┘ └─┘
src └──────────┘└──────────────┘└─┘ ┴ └
typ └──────────┘└──────────────┘└─┘└─┘┴└─┘└
doc └──────────┘ └─┘ ┴ └
txt └──────────┘ └─┘ ┴ └
par └──────────┘ └─┘ ┴ └
pid ┴└────┘ └─┘ ┴ └
st └───────────────────────────────────────
207
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
208 private lemma eisenstein_lemma_aux₁ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ}
id ┴ ┴└────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴
typ ┴ ┴└────┘ ┴ ┴ ┴ ┴
doc └────┘
209 (hap : (a : zmodp p hp) ≠ 0) :
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
210 (((Ico 1 (p / 2).succ).sum (λ x, a * x) : ℕ) : zmod 2) =
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └─┘
211 ((Ico 1 (p / 2).succ).filter
id └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
212 ((λ x : ℕ, p / 2 < (a * x : zmodp p hp).val))).card +
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴
doc └──┘
213 (Ico 1 (p / 2).succ).sum (λ x, x)
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴
src └─┘ ┴ └──┘ └─┘
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴
doc └─┘
214 + ((Ico 1 (p / 2).succ).sum (λ x, (a * x) / p) : ℕ) :=
id ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
215 have hp2 : (p : zmod 2) = (1 : ℕ), from zmod.eq_iff_modeq_nat.2 hp2,
id ┴ └──┘ ┴ ┴ └───────────────────┘┴ └─┘
src └──┘ ┴ ┴ └───────────────────┘┴
typ ┴ └──┘ ┴ ┴ └───────────────────┘┴ └─┘
216 calc (((Ico 1 (p / 2).succ).sum (λ x, a * x) : ℕ) : zmod 2)
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ ┴ └──┘ └─┘ ┴ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─┘
217 = (((Ico 1 (p / 2).succ).sum (λ x, (a * x) % p + p * ((a * x) / p)) : ℕ) : zmod 2) :
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─┘
218 by simp only [mod_add_div]
id └─────────┘
src └─────────┘└─────────┘└┘
typ └─────────┘└─────────┘└┘
doc └─────────┘ └┘
txt └─────────┘ └┘
par └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st └───────────────────────┘
219 ... = ((Ico 1 (p / 2).succ).sum (λ x, ((a * x : ℕ) : zmodp p hp).val) : ℕ) +
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ └───┘ └─┘ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴
doc └─┘
220 ((Ico 1 (p / 2).succ).sum (λ x, (a * x) / p) : ℕ) :
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
221 by simp only [zmodp.val_cast_nat];
id └────────────────┘
src └─────────┘└────────────────┘┴
typ └─────────┘└────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st └────────────────────────────────
222 simp [sum_add_distrib, mul_sum.symm, nat.cast_add, nat.cast_mul, sum_nat_cast, hp2]
id └─────────────┘ └──────────┘ └──────────┘ └──────────┘ └─┘
src └────┘└─────────────┘└┘ └┘└──────────┘└┘└──────────┘└┘└──────────┘└┘ └┘
typ └────┘└─────────────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└┘└─┘└┘
doc └────┘ └┘ └┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────────────┘
223 ... = _ : congr_arg2 (+)
id └────────┘ ┴
src └────────┘ ┴
typ └────────┘ ┴
224 (calc (((Ico 1 (p / 2).succ).sum (λ x, ((a * x : ℕ) : zmodp p hp).val) : ℕ) : zmod 2)
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ └──┘
src └─┘ ┴ └──┘ └─┘ ┴ ┴ └───┘ └─┘ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ └──┘
doc └─┘
225 = (Ico 1 (p / 2).succ).sum
id └─┘ ┴ ┴ └──┘ └─┘
src └─┘ ┴ └──┘ └─┘
typ └─┘ ┴ ┴ └──┘ └─┘
doc └─┘
226 (λ x, ((((a * x : zmodp p hp).val_min_abs +
id ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ ┴
src ┴ └───┘ └─────────┘ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ ┴
doc └─────────┘
227 (if (a * x : zmodp p hp).val ≤ p / 2 then 0 else p)) : ℤ) : zmod 2)) :
id ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ └───┘ └─┘ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
228 by simp only [(zmodp.val_eq_ite_val_min_abs _).symm]; simp [sum_nat_cast]
id └──────────────────────────┘ └──────────┘
src └─────────┘ └──────────────────────────┘└───────┘ └────┘└──────────┘└─
typ └─────────┘ └──────────────────────────┘└───────┘ └────┘└──────────┘└─
doc └─────────┘ └───────┘ └────┘ └─
txt └─────────┘ └───────┘ └────┘ └─
par └─────────┘ └───────┘ └────┘ └─
pid ┴└──┘└┘ └───────┘ ┴┴ ┴└
st └───────────────────────────────────────────────────────────────────────
229 ... = ((Ico 1 (p / 2).succ).filter
id └─┘ ┴ ┴ └──┘ └────┘
src ─┘ └─┘ ┴ └──┘ └────┘
typ ─┘ └─┘ ┴ ┴ └──┘ └────┘
doc ─┘ └─┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
230 (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card +
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴
doc └──┘
231 (((Ico 1 (p / 2).succ).sum (λ x, (a * x : zmodp p hp).val_min_abs.nat_abs)) : ℕ) :
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ ┴
src └─┘ ┴ └──┘ └─┘ ┴ └───┘ └─────────┘ └─────┘ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─────────┘ └─────┘ ┴
doc └─┘ └─────────┘
232 by simp [sum_add_distrib, finset.sum_ite, hp2, sum_nat_cast]
id └─────────────┘ └────────────┘ └─┘ └──────────┘
src └────┘└─────────────┘└┘└────────────┘└┘ └┘└──────────┘└─
typ └────┘└─────────────┘└┘└────────────┘└┘└─┘└┘└──────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────
233 ... = _ : by rw [finset.sum_eq_multiset_sum,
id └────────────────────────┘
src ─┘ └──┘└────────────────────────┘└─
typ ─┘ └──┘└────────────────────────┘└─
doc ─┘ └──┘ └─
txt ─┘ └──┘ └─
par ─┘ └──┘ └─
pid ─┘ └┘ └─
st ─┘ └─────────────────────────────┘└─
234 Ico_map_val_min_abs_nat_abs_eq_Ico_map_id hp _ hap,
id └───────────────────────────────────────┘ └┘ └─┘
src ─────┘└───────────────────────────────────────┘┴ └─┘ └─
typ ─────┘└───────────────────────────────────────┘┴└┘└─┘└─┘└─
doc ─────┘└───────────────────────────────────────┘┴ └─┘ └─
txt ─────┘ ┴ └─┘ └─
par ─────┘ ┴ └─┘ └─
pid ─────┘ ┴ └─┘ └─
st ───────────────────────────────────────────────────────┘└─
235 ← finset.sum_eq_multiset_sum];
id └────────────────────────┘
src ───────┘└────────────────────────┘┴
typ ───────┘└────────────────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ─────────────────────────────────┘┴└─
236 simp [sum_nat_cast]) rfl
id └──────────┘ └─┘
src └────┘└──────────┘┴ └─┘
typ └────┘└──────────┘┴ └─┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────────┘
237
238 private lemma eisenstein_lemma_aux₂ {p : ℕ} (hp : p.prime) (hp2 : p % 2 = 1) {a : ℕ} (ha2 : a % 2 = 1)
id ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
239 (hap : (a : zmodp p hp) ≠ 0) :
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
240 ((Ico 1 (p / 2).succ).filter
id └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
241 ((λ x : ℕ, p / 2 < (a * x : zmodp p hp).val))).card
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
doc └──┘
242 ≡ (Ico 1 (p / 2).succ).sum (λ x, (x * a) / p) [MOD 2] :=
id ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ └─┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴
typ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc ┴ └─┘ └──┘ ┴
243 have ha2 : (a : zmod 2) = (1 : ℕ), from zmod.eq_iff_modeq_nat.2 ha2,
id ┴ └──┘ ┴ ┴ └───────────────────┘┴ └─┘
src └──┘ ┴ ┴ └───────────────────┘┴
typ ┴ └──┘ ┴ ┴ └───────────────────┘┴ └─┘
244 (@zmod.eq_iff_modeq_nat 2 _ _).1 $ sub_eq_zero.1 $
id └───────────────────┘ ┴ └─────────┘┴
src └───────────────────┘ ┴ └─────────┘┴
typ └───────────────────┘ ┴ └─────────┘┴
245 by simpa [finset.mul_sum.symm, mul_comm, ha2, sum_nat_cast, add_neg_eq_iff_eq_add.symm,
id └──────┘ └─┘ └──────────┘
src └─────┘ └┘└──────┘└┘ └┘└──────────┘└┘ └─
typ └─────┘└─────────────────┘└┘└──────┘└┘└─┘└┘└──────────┘└┘└────────────────────────┘└─
doc └─────┘ └┘ └┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ └─
st └─────────────────────────────────────────────────────────────────────────────────────
246 zmod.neg_eq_self_mod_two] using eq.symm (eisenstein_lemma_aux₁ hp hp2 hap)
id └──────────────────────┘ └─────┘ └───────────────────┘ └┘ └─┘ └─┘
src ───┘└──────────────────────┘└──────┘└─────┘┴ └───────────────────┘┴ ┴ ┴ └─
typ ───┘└──────────────────────┘└──────┘└─────┘┴ └───────────────────┘┴└┘┴└─┘┴└─┘└─
doc ───┘ └──────┘ ┴ ┴ ┴ ┴ └─
txt ───┘ └──────┘ ┴ ┴ ┴ ┴ └─
par ───┘ └──────┘ ┴ ┴ ┴ ┴ └─
pid ───┘ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴└
st ───────────────────────────────────────────────────────────────────────────────
247
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
248 lemma div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b =
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
249 ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :=
id └─┘ ┴└───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ └───┘ └────┘ ┴ ┴ └──┘
typ └─┘ ┴└───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─┘ └────┘ └──┘
250 calc a / b = (Ico 1 (a / b).succ).card : by simp
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └──┘
src ┴ └─┘ ┴ └──┘ └──┘ └───┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └──┘ └───┘
doc └─┘ └──┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
251 ... = ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :
id └─┘ ┴└───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ └───┘ └────┘ ┴ ┴ └──┘
typ └─┘ ┴└───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─┘ └────┘ └──┘
252 congr_arg _$ finset.ext.2 $ λ x,
id └───────┘ └────────┘┴ ┴
src └───────┘ └────────┘┴
typ └───────┘ └────────┘┴ ┴
253 have x * b ≤ a → x ≤ c,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
254 from λ h, le_trans (by rwa [le_div_iff_mul_le _ _ hb0]) hc,
id ┴ └──────┘ └───────────────┘ └─┘ └┘
src └──────┘ └───┘└───────────────┘└───┘ ┴
typ ┴ └──────┘ └───┘└───────────────┘└───┘└─┘┴ └┘
doc └───┘ └───┘ ┴
txt └───┘ └───┘ ┴
par └───┘ └───┘ ┴
pid └┘ └───┘ ┴
st └─────────────────────────────┘┴
255 by simp [lt_succ_iff, le_div_iff_mul_le _ _ hb0]; tauto
id └─────────┘ └───────────────┘ └─┘
src └────┘└─────────┘└┘└───────────────┘└───┘ ┴ └─────
typ └────┘└─────────┘└┘└───────────────┘└───┘└─┘┴ └─────
doc └────┘ └┘ └───┘ ┴ └─────
txt └────┘ └┘ └───┘ ┴ └─────
par └────┘ └┘ └───┘ ┴ └─────
pid ┴┴ └┘ └───┘ ┴ └
st └─────────────────────────────────────────────────────
256
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
257 /-- The given sum is the number of integers point in the triangle formed by the diagonal of the
258 rectangle `(0, p/2) × (0, q/2)` -/
259 private lemma sum_Ico_eq_card_lt {p q : ℕ} :
id ┴
src ┴
typ ┴
260 (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) =
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
261 (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
262 (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)).card :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
doc └──┘
263 if hp0 : p = 0 then by simp [hp0, finset.ext]
id └┘ ┴ ┴ └─┘ └────────┘
src └┘ ┴ └────┘ └┘└────────┘└┘
typ └┘ ┴ ┴ └────┘└─┘└┘└────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └──────────────────────┘
264 else
265 calc (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) =
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
266 (Ico 1 (p / 2).succ).sum (λ a,
id └─┘ ┴ ┴ └──┘ └─┘ ┴
src └─┘ ┴ └──┘ └─┘
typ └─┘ ┴ ┴ └──┘ └─┘ ┴
doc └─┘
267 ((Ico 1 (q / 2).succ).filter (λ x, x * p ≤ a * q)).card) :
id └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ ┴ └──┘ └────┘ ┴ ┴ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─┘ └────┘ └──┘
268 finset.sum_congr rfl $ λ x hx,
id └──────────────┘ └─┘ ┴ └┘
src └──────────────┘ └─┘
typ └──────────────┘ └─┘ ┴ └┘
269 div_eq_filter_card (nat.pos_of_ne_zero hp0)
id └────────────────┘ └────────────────┘ └─┘
src └────────────────┘ └────────────────┘
typ └────────────────┘ └────────────────┘ └─┘
270 (calc x * q / p ≤ (p / 2) * q / p :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
271 nat.div_le_div_right (mul_le_mul_of_nonneg_right
id └──────────────────┘ └────────────────────────┘
src └──────────────────┘ └────────────────────────┘
typ └──────────────────┘ └────────────────────────┘
272 (le_of_lt_succ $ by finish)
id └───────────┘
src └───────────┘ └────┘
typ └───────────┘ └────┘
doc └────┘
txt └────┘
par └────┘
st └─────┘
273 (nat.zero_le _))
id └─────────┘
src └─────────┘
typ └─────────┘
274 ... ≤ _ : nat.div_mul_div_le_div _ _ _)
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
275 ... = _ : by rw [← card_sigma];
id └─┘ └────────┘
src └─┘ └────┘└────────┘┴
typ └─┘ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st └───────────────┘┴└─
276 exact card_congr (λ a _, ⟨a.1, a.2⟩)
id └────────┘
src └────┘└────────┘┴ └────┘ └──┘ └────
typ └────┘└────────┘┴ └────┘ └──┘ └────
doc └────┘ ┴ └────┘ └──┘ └────
txt └────┘ ┴ └────┘ └──┘ └────
par └────┘ ┴ └────┘ └──┘ └────
pid ┴ ┴ └────┘ └──┘ └────
st ─────────────────────────────────────────
277 (by simp {contextual := tt})
id └┘
src ─────┘ ┴└───┘ └────────────┘└┘┴└─
typ ─────┘ ┴└───┘ └────────────┘└┘┴└─
doc ─────┘ ┴└───┘ └────────────┘ ┴└─
txt ─────┘ ┴└───┘ └────────────┘ ┴└─
par ─────┘ ┴└───┘ └────────────┘ ┴└─
pid ─────┘ └────┘ └────────────┘ └──
st ────────┘└──────────────────────┘└─
278 (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
id └┘
src ─────┘ └──────────────┘ ┴└───┘ └────────────┘└┘┴└─
typ ─────┘ └──────────────┘ ┴└───┘ └────────────┘└┘┴└─
doc ─────┘ └──────────────┘ ┴└───┘ └────────────┘ ┴└─
txt ─────┘ └──────────────┘ ┴└───┘ └────────────┘ ┴└─
par ─────┘ └──────────────┘ ┴└───┘ └────────────┘ ┴└─
pid ─────┘ └──────────────┘ └────┘ └────────────┘ └──
st ─────────────────────────┘└──────────────────────┘└─
279 (λ ⟨b₁, b₂⟩ h, ⟨⟨b₁, b₂⟩,
id └┘ └┘
src ─────┘ └┘ └┘ └───┘ └┘ └──
typ ─────┘ └┘└┘└┘└┘└───┘ └┘ └──
doc ─────┘ └┘ └┘ └───┘ └┘ └──
txt ─────┘ └┘ └┘ └───┘ └┘ └──
par ─────┘ └┘ └┘ └───┘ └┘ └──
pid ─────┘ └┘ └┘ └───┘ └┘ └──
st ────────────────────────────────
280 by revert h; simp {contextual := tt}⟩)
id └┘
src ───────┘ ┴└──────┘└┘└───┘ └────────────┘└┘┴└──
typ ───────┘ ┴└──────┘└┘└───┘ └────────────┘└┘┴└──
doc ───────┘ ┴└──────┘└┘└───┘ └────────────┘ ┴└──
txt ───────┘ ┴└──────┘└┘└───┘ └────────────┘ ┴└──
par ───────┘ ┴└──────┘└┘└───┘ └────────────┘ ┴└──
pid ───────┘ └──────────────┘ └────────────┘ └─┘└
st ─────────┘└────────────────────────────────┘└──
281
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
282 /-- Each of the sums in this lemma is the cardinality of the set integer points in each of the
283 two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them
284 gives the number of points in the rectangle. -/
285 private lemma sum_mul_div_add_sum_mul_div_eq_mul {p q : ℕ} (hp : p.prime)
id ┴ ┴└────┘
src ┴ └────┘
typ ┴ ┴└────┘
doc └────┘
286 (hq0 : (q : zmodp p hp) ≠ 0) :
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
287 (Ico 1 (p / 2).succ).sum (λ a, (a * q) / p) +
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
288 (Ico 1 (q / 2).succ).sum (λ a, (a * p) / q) =
id └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
289 (p / 2) * (q / 2) :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
290 have hswap : (((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
291 (λ x : ℕ × ℕ, x.2 * q ≤ x.1 * p)).card =
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
doc └──┘
292 (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
293 (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)).card :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
doc └──┘
294 card_congr (λ x _, prod.swap x)
id └────────┘ ┴ ┴ └───────┘ ┴
src └────────┘ └───────┘
typ └────────┘ ┴ ┴ └───────┘ ┴
doc └───────┘
295 (λ ⟨_, _⟩, by simp {contextual := tt})
id ┴ └┘
src └───┘ └────────────┘└┘┴
typ ┴ └───┘ └────────────┘└┘┴
doc └───┘ └────────────┘ ┴
txt └───┘ └────────────┘ ┴
par └───┘ └────────────┘ ┴
pid ┴ └────────────┘ ┴
st └──────────────────────┘
296 (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
id ┴ ┴ └┘
src └───┘ └────────────┘└┘┴
typ ┴ ┴ └───┘ └────────────┘└┘┴
doc └───┘ └────────────┘ ┴
txt └───┘ └────────────┘ ┴
par └───┘ └────────────┘ ┴
pid ┴ └────────────┘ ┴
st └──────────────────────┘
297 (λ ⟨x₁, x₂⟩ h, ⟨⟨x₂, x₁⟩, by revert h; simp {contextual := tt}⟩),
id ┴└┘ └┘ ┴ └┘
src └──────┘ └───┘ └────────────┘└┘┴
typ ┴└┘ └┘ ┴ └──────┘ └───┘ └────────────┘└┘┴
doc └──────┘ └───┘ └────────────┘ ┴
txt └──────┘ └───┘ └────────────┘ ┴
par └──────┘ └───┘ └────────────┘ ┴
pid └┘ ┴ └────────────┘ ┴
st └────────────────────────────────┘
298 have hdisj : disjoint
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
299 (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
300 (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q))
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
301 (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
302 (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)),
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴
303 from disjoint_filter.2 $ λ x hx hpq hqp,
id └─────────────┘┴ ┴ └┘ └─┘ └─┘
src └─────────────┘┴
typ └─────────────┘┴ ┴ └┘ └─┘ └─┘
304 have hxp : x.1 < p, from lt_of_le_of_lt
id ┴┴ ┴ ┴ └────────────┘
src ┴ ┴ └────────────┘
typ ┴┴ ┴ ┴ └────────────┘
305 (show x.1 ≤ p / 2, by simp [*, nat.lt_succ_iff] at *; tauto)
id ┴┴ ┴ ┴ ┴ └─────────────┘
src ┴ ┴ ┴ └───────┘└─────────────┘└────┘ └───┘
typ ┴┴ ┴ ┴ ┴ └───────┘└─────────────┘└────┘ └───┘
doc └───────┘ └────┘ └───┘
txt └───────┘ └────┘ └───┘
par └───────┘ └────┘ └───┘
pid ┴└──┘ ┴┴└──┘
st └────────────────────────────────────┘
306 (nat.div_lt_self hp.pos dec_trivial),
id └─────────────┘ └┘└──┘ └─────────┘
src └─────────────┘ └──┘ └─────────┘
typ └─────────────┘ └┘└──┘ └─────────┘
doc └─────────┘
307 begin
st └─────
308 have : (x.1 : zmodp p hp) = 0,
id ┴ └───┘ ┴ └┘ ┴
src └─────┘ └───┘└───┘┴ ┴ └┘┴└┘
typ └─────┘ ┴└───┘└───┘┴┴┴└┘└┘┴└┘
doc └─────┘ └───┘ ┴ ┴ └┘ └┘
txt └─────┘ └───┘ ┴ ┴ └┘ └┘
par └─────┘ └───┘ ┴ ┴ └┘ └┘
pid └───┘└┘ └───┘ ┴ ┴ └┘ ┴┴
st ────────────────────────────────┘└─
309 { simpa [hq0] using congr_arg (coe : ℕ → zmodp p hp) (le_antisymm hpq hqp) },
id └─┘ └───────┘ └─┘ └───┘ ┴ └┘ └─────────┘ └─┘ └─┘
src └─────┘ └──────┘└───────┘┴ └─┘└─┘ ┴ ┴└───┘┴ ┴ └┘ └─────────┘┴ ┴ └┘
typ └─────┘└─┘└──────┘└───────┘┴ └─┘└─┘ ┴ ┴└───┘┴┴┴└┘└┘ └─────────┘┴└─┘┴└─┘└┘
doc └─────┘ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
txt └─────┘ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
par └─────┘ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
pid ┴┴ ┴┴└────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴
st ─────┘└───────────────────────────────────────────────────────────────────────┘└┘└
310 rw [fin.eq_iff_veq, zmodp.val_cast_of_lt hp hxp, zmodp.zero_val] at this,
id └────────────┘ └──────────────────┘ └┘ └─┘ └────────────┘
src └──┘└────────────┘└┘└──────────────────┘┴ ┴ └┘└────────────┘└───────┘
typ └──┘└────────────┘└┘└──────────────────┘┴└┘┴└─┘└┘└────────────┘└───────┘
doc └──┘ └┘ ┴ ┴ └┘ └───────┘
txt └──┘ └┘ ┴ ┴ └┘ └───────┘
par └──┘ └┘ ┴ ┴ └┘ └───────┘
pid └┘ └┘ ┴ ┴ └┘ ┴└──────┘
st ─────────────────────┘└───────────────────────────┘└──────────────┘┴└──────┘└─
311 simp * at *
src └───────────
typ └───────────
doc └───────────
txt └───────────
par └───────────
pid ┴┴┴└──┘└
st ────────────────
312 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
313 have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
314 (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q) ∪
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
315 ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘ └────┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └─────┘ └─┘ └────┘
316 (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) =
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
317 ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)),
id └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘
src └─┘ ┴ └──┘ └─────┘ └─┘ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └─────┘ └─┘ ┴ ┴ └──┘
doc └─┘ └─────┘ └─┘
318 from finset.ext.2 $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
id └────────┘┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └────────┘┴ └──────┘└──────┘┴ └─┘┴┴ └┘ └─┘ ┴ ┴ └──┘ └───┘
typ └────────┘┴ ┴ └──────┘└──────┘┴ └─┘┴┴┴└┘ ┴└─┘ ┴┴┴ └──┘ └───┘
doc └──────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └──┘ └───┘
txt └──────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └──┘ └───┘
par └──────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └──┘ └───┘
pid └───┘└─┘ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴
st └────────────────────────────────────────────────┘
319 by rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
id └────────────────┘ └────────────────┘ └───┘ └─────────────────┘ └───┘ └────┘
src └──┘└────────────────┘└┘└────────────────┘└┘ └──┘└─────────────────┘┴ └┘ └─
typ └──┘└────────────────┘└┘└────────────────┘└┘└───┘└──┘└─────────────────┘┴└───┘└┘└────┘└─
doc └──┘└────────────────┘└┘└────────────────┘└┘ └──┘ ┴ └┘ └─
txt └──┘ └┘ └┘ └──┘ ┴ └┘ └─
par └──┘ └┘ └┘ └──┘ ┴ └┘ └─
pid └┘ └┘ └┘ └──┘ ┴ └┘ └─
st └─────────────────────┘└──────────────────┘└─────┘└───────────────────────────┘└──────┘└─
320 card_product];
id └──────────┘
src ───┘└──────────┘┴
typ ───┘└──────────┘┴
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ───────────────┘┴└─
321 simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ───────
322
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
323 variables {p q : ℕ} (hp : nat.prime p) (hq : nat.prime q)
id ┴ ┴ └───────┘ └───────┘
src ┴ └───────┘ └───────┘
typ ┴ ┴ └───────┘ └───────┘
doc └───────┘ └───────┘
324
325 namespace zmodp
326
327 def legendre_sym (a p : ℕ) (hp : nat.prime p) : ℤ :=
id ┴ └───────┘ ┴ ┴
src ┴ └───────┘ ┴
typ ┴ └───────┘ ┴ ┴
doc └───────┘
328 if (a : zmodp p hp) = 0 then 0 else if ∃ b : zmodp p hp, b ^ 2 = a then 1 else -1
id ┴ └───┘ ┴ └┘ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ └┘ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴
329
330 lemma legendre_sym_eq_pow (a p : ℕ) (hp : nat.prime p) :
id ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ └───────┘ ┴
doc └───────┘
331 (legendre_sym a p hp : zmodp p hp) = (a ^ (p / 2)) :=
id └──────────┘ ┴ ┴ └┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └───┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ └┘ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
332 if ha : (a : zmodp p hp) = 0 then by simp [*, legendre_sym, _root_.zero_pow (nat.div_pos hp.two_le (succ_pos 1))]
id └┘ ┴ └───┘ ┴ └┘ ┴ └──────────┘ └─────────────┘ └─────────┘ └───────┘ └──────┘
src └┘ └───┘ ┴ └───────┘└──────────┘└┘└─────────────┘┴ └─────────┘┴└───────┘┴ └──────┘└────┘
typ └┘ ┴ └───┘ ┴ └┘ ┴ └───────┘└──────────┘└┘└─────────────┘┴ └─────────┘┴└───────┘┴ └──────┘└────┘
doc └───────┘ └┘ ┴ ┴ ┴ └────┘
txt └───────┘ └┘ ┴ ┴ ┴ └────┘
par └───────┘ └┘ ┴ ┴ ┴ └────┘
pid ┴└──┘ └┘ ┴ ┴ ┴ └───┘┴
st └────────────────────────────────────────────────────────────────────────────┘
333 else
334 (nat.prime.eq_two_or_odd hp).elim
id └─────────────────────┘ └┘ └──┘
src └─────────────────────┘ └──┘
typ └─────────────────────┘ └┘ └──┘
335 (λ hp2, begin resetI; subst hp2,
id └─┘ └─┘
src └────┘ └────┘
typ └─┘ └────┘ └────┘└─┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴
st └─────────────────────┘└─
336 suffices : ∀ a : zmodp 2 nat.prime_two,
id └───┘
src └─────────┘ └───┘ └─┘ └
typ └─────────┘ └───┘└───┘└─┘ └
doc └─────────┘ └───┘ └─┘ └
txt └─────────┘ └───┘ └─┘ └
par └─────────┘ └───┘ └─┘ └
pid └───────┘└┘ └───┘ └─┘ └
st ────────────────────────────────────────────
337 (((ite (a = 0) 0 (ite (∃ (b : zmodp 2 hp), b ^ 2 = a) 1 (-1))) : ℤ) : zmodp 2 nat.prime_two) = a ^ (2 / 2),
id ┴ └─┘ ┴ └───┘ └┘ ┴ ┴ ┴ └───────────┘ ┴
src ─────┘ ┴ ┴┴└────┘ └─┘┴ ┴└────┘└───┘└─┘ ┴┴┴ ┴┴└─┘ ┴ └──┘ ┴└─────┘ └──┘ └─┘└───────────┘└┘ ┴ ┴ ┴ └┘┴└─┘
typ ─────┘ ┴ ┴┴└────┘ └─┘┴ ┴└────┘└───┘└─┘└┘┴┴┴ ┴┴└─┘ ┴ └──┘ ┴└─────┘ └──┘ └─┘└───────────┘└┘ ┴ ┴ ┴ └┘┴└─┘
doc ─────┘ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └─────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ └┘ └─┘
txt ─────┘ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └─────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ └┘ └─┘
par ─────┘ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └─────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ └┘ └─┘
pid ─────┘ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └─────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ └┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
338 { exact this a },
id └──┘ ┴
src └────┘ ┴ ┴
typ └────┘└──┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└───────────┘└┘└
339 exact dec_trivial,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘└─────────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────┘└─
340 end)
st ─────┘
341 (λ hp1, have _ := euler_criterion hp ha,
id └─┘ └─────────────┘ └┘ └┘
src └─────────────┘
typ └─┘ └─────────────┘ └┘ └┘
342 have (-1 : zmodp p hp) ≠ 1, from (ne_neg_self hp hp1 zero_ne_one.symm).symm,
id ┴ └───┘ ┴ └┘ ┴ └─────────┘ └┘ └─┘ └─────────┘└───┘ └──┘
src ┴ └───┘ ┴ └─────────┘ └─────────┘└───┘ └──┘
typ ┴ └───┘ ┴ └┘ ┴ └─────────┘ └┘ └─┘ └─────────┘└───┘ └──┘
343 by cases zmodp.pow_div_two_eq_neg_one_or_one hp ha; simp [legendre_sym, *] at *)
id └─────────────────────────────────┘ └┘ └┘ └──────────┘
src └────┘└─────────────────────────────────┘┴ ┴ └────┘└──────────┘└───────┘
typ └────┘└─────────────────────────────────┘┴└┘┴└┘ └────┘└──────────┘└───────┘
doc └────┘ ┴ ┴ └────┘ └───────┘
txt └────┘ ┴ ┴ └────┘ └───────┘
par └────┘ ┴ ┴ └────┘ └───────┘
pid ┴ ┴ ┴ ┴┴ └──┘┴└──┘
st └───────────────────────────────────────────────────────────────────────────┘
344
345 lemma legendre_sym_eq_one_or_neg_one (a : ℕ) (hp : nat.prime p) (ha : (a : zmodp p hp) ≠ 0) :
id ┴ └───────┘ ┴ ┴ └───┘ ┴ └┘ ┴
src ┴ └───────┘ └───┘ ┴
typ ┴ └───────┘ ┴ ┴ └───┘ ┴ └┘ ┴
doc └───────┘
346 legendre_sym a p hp = -1 ∨ legendre_sym a p hp = 1 :=
id └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴
src └──────────┘ ┴ ┴ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴
347 by unfold legendre_sym; split_ifs; simp * at *
src └─────────────────┘ └───────┘ └───────────
typ └─────────────────┘ └───────┘ └───────────
doc └─────────────────┘ └───────┘ └───────────
txt └─────────────────┘ └───────┘ └───────────
par └─────────────────┘ └───────┘ └───────────
pid └───────────┘ ┴┴┴└──┘└
st └────────────────────────────────────────────
348
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
349 /-- Gauss' lemma. The legendre symbol can be computed by considering the number of naturals less
350 than `p/2` such that `(a * x) % p > p / 2` -/
351 lemma gauss_lemma {a : ℕ} (hp1 : p % 2 = 1) (ha0 : (a : zmodp p hp) ≠ 0) :
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
src ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
352 legendre_sym a p hp = (-1) ^ ((Ico 1 (p / 2).succ).filter
id └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src └──────────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └────┘
typ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
353 (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘
doc └──┘
354 have (legendre_sym a p hp : zmodp p hp) = (((-1)^((Ico 1 (p / 2).succ).filter
id └──────────┘ ┴ ┴ └┘ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
src └──────────┘ └───┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └────┘
typ └──────────┘ ┴ ┴ └┘ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
doc └─┘ └────┘
355 (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card : ℤ) : zmodp p hp),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴ └───┘ ┴ └┘
src ┴ ┴ ┴ ┴ └───┘ └─┘ └──┘ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ └──┘ ┴ └───┘ ┴ └┘
doc └──┘
356 by rw [legendre_sym_eq_pow, gauss_lemma_aux₂ hp hp1 ha0]; simp,
id └─────────────────┘ └──────────────┘ └┘ └─┘ └─┘
src └──┘└─────────────────┘└┘└──────────────┘┴ ┴ ┴ ┴ └──┘
typ └──┘└─────────────────┘└┘└──────────────┘┴└┘┴└─┘┴└─┘┴ └──┘
doc └──┘ └┘ ┴ ┴ ┴ ┴ └──┘
txt └──┘ └┘ ┴ ┴ ┴ ┴ └──┘
par └──┘ └┘ ┴ ┴ ┴ ┴ └──┘
pid └┘ └┘ ┴ ┴ ┴ ┴
st └──────────────────────┘└───────────────────────────┘┴└────┘
357 begin
st └─────
358 cases legendre_sym_eq_one_or_neg_one a hp ha0;
id └────────────────────────────┘ ┴ └┘ └─┘
src └────┘└────────────────────────────┘┴ ┴ ┴
typ └────┘└────────────────────────────┘┴┴┴└┘┴└─┘
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────
359 cases @neg_one_pow_eq_or ℤ _ ((Ico 1 (p / 2).succ).filter
id └───────────────┘ └─┘ ┴
src └────┘ └───────────────┘┴ └──┘ └─┘└─┘ ┴┴└────────────────
typ └────┘ └───────────────┘┴ └──┘ └─┘└─┘ ┴┴└────────────────
doc └────┘ ┴ └──┘ └─┘└─┘ ┴ └────────────────
txt └────┘ ┴ └──┘ └─┘ ┴ └────────────────
par └────┘ ┴ └──┘ └─┘ ┴ └────────────────
pid ┴ ┴ └──┘ └─┘ ┴ └────────────────
st ─────────────────────────────────────────────────────────────
360 (λ x : ℕ, p / 2 < (a * x : zmodp p hp).val)).card;
id ┴ ┴ ┴ └───┘ ┴ └┘
src ───┘ └───┘ └┘ ┴ └─┘┴┴ ┴┴┴ └─┘└───┘┴ ┴ └──────────┘
typ ───┘ └───┘ └┘ ┴ └─┘┴┴ ┴┴┴┴ └─┘└───┘┴┴┴└┘└──────────┘
doc ───┘ └───┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────────┘
txt ───┘ └───┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────────┘
par ───┘ └───┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────────┘
pid ───┘ └───┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─────────┘┴
st ───────────────────────────────────────────────────────
361 simp [*, zmodp.ne_neg_self hp hp1 one_ne_zero,
id └───────────────┘ └┘ └─┘ └─────────┘
src └───────┘└───────────────┘┴ ┴ ┴└─────────┘└─
typ └───────┘└───────────────┘┴└┘┴└─┘┴└─────────┘└─
doc └───────┘ ┴ ┴ ┴ └─
txt └───────┘ ┴ ┴ ┴ └─
par └───────┘ ┴ ┴ ┴ └─
pid ┴└──┘ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────
362 (zmodp.ne_neg_self hp hp1 one_ne_zero).symm] at *
id └───────────────┘ └┘ └─┘ └─────────┘
src ───┘ └───────────────┘┴ ┴ ┴└─────────┘└───────────┘
typ ───┘ └───────────────┘┴└┘┴└─┘┴└─────────┘└───────────┘
doc ───┘ ┴ ┴ ┴ └───────────┘
txt ───┘ ┴ ┴ ┴ └───────────┘
par ───┘ ┴ ┴ ┴ └───────────┘
pid ───┘ ┴ ┴ ┴ └─────┘┴└──┘┴
st ─────────────────────────────────────────────────────┘
363 end
st └─┘
364
365 lemma legendre_sym_eq_one_iff {a : ℕ} (ha0 : (a : zmodp p hp) ≠ 0) :
id ┴ ┴ └───┘ ┴ └┘ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ └┘ ┴
366 legendre_sym a p hp = 1 ↔ (∃ b : zmodp p hp, b ^ 2 = a) :=
id └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
367 by rw [legendre_sym]; split_ifs; finish
id └──────────┘
src └──┘└──────────┘┴ └───────┘ └──────
typ └──┘└──────────┘┴ └───────┘ └──────
doc └──┘ ┴ └───────┘ └──────
txt └──┘ ┴ └───────┘ └──────
par └──┘ ┴ └───────┘ └──────
pid └┘ ┴ └
st └───────────────┘┴└───────────────────
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 lemma eisenstein_lemma (hp1 : p % 2 = 1) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : zmodp p hp) ≠ 0) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
370 legendre_sym a p hp = (-1)^(Ico 1 (p / 2).succ).sum (λ x, (x * a) / p) :=
id └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ └─┘ ┴ └──┘ └─┘ ┴ ┴
typ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
371 by rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp hp1 ha0, neg_one_pow_eq_pow_mod_two,
id └────────────────────────┘ └─────────┘ └┘ └─┘ └─┘ └────────────────────────┘
src └──┘└────────────────────────┘└┘└─────────┘┴ ┴ ┴ └┘└────────────────────────┘└─
typ └──┘└────────────────────────┘└┘└─────────┘┴└┘┴└─┘┴└─┘└┘└────────────────────────┘└─
doc └──┘ └┘└─────────┘┴ ┴ ┴ └┘ └─
txt └──┘ └┘ ┴ ┴ ┴ └┘ └─
par └──┘ └┘ ┴ ┴ ┴ └┘ └─
pid └┘ └┘ ┴ ┴ ┴ └┘ └─
st └─────────────────────────────┘└──────────────────────┘└──────────────────────────┘└─
372 show _ = _, from eisenstein_lemma_aux₂ hp hp1 ha1 ha0]
id ┴ └───────────────────┘ └┘ └─┘ └─┘ └─┘
src ───┘ └─┘┴└───────┘└───────────────────┘┴ ┴ ┴ ┴ └─
typ ───┘ └─┘┴└───────┘└───────────────────┘┴└┘┴└─┘┴└─┘┴└─┘└─
doc ───┘ └─┘ └───────┘ ┴ ┴ ┴ ┴ └─
txt ───┘ └─┘ └───────┘ ┴ ┴ ┴ ┴ └─
par ───┘ └─┘ └───────┘ ┴ ┴ ┴ ┴ └─
pid ───┘ └─┘ └───────┘ ┴ ┴ ┴ ┴ ┴└
st ────────────────────────────────────────────────────────┘┴└
373
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
374 theorem quadratic_reciprocity (hp1 : p % 2 = 1) (hq1 : q % 2 = 1) (hpq : p ≠ q) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
375 legendre_sym p q hq * legendre_sym q p hp = (-1) ^ ((p / 2) * (q / 2)) :=
id └──────────┘ ┴ ┴ └┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ └┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
376 have hpq0 : (p : zmodp q hq) ≠ 0, from zmodp.prime_ne_zero _ hp hpq.symm,
id ┴ └───┘ ┴ └┘ ┴ └─────────────────┘ └┘ └─┘└───┘
src └───┘ ┴ └─────────────────┘ └───┘
typ ┴ └───┘ ┴ └┘ ┴ └─────────────────┘ └┘ └─┘└───┘
377 have hqp0 : (q : zmodp p hp) ≠ 0, from zmodp.prime_ne_zero _ hq hpq,
id ┴ └───┘ ┴ └┘ ┴ └─────────────────┘ └┘ └─┘
src └───┘ ┴ └─────────────────┘
typ ┴ └───┘ ┴ └┘ ┴ └─────────────────┘ └┘ └─┘
378 by rw [eisenstein_lemma _ hq1 hp1 hpq0, eisenstein_lemma _ hp1 hq1 hqp0,
id └──────────────┘ └─┘ └─┘ └──┘ └──────────────┘ └─┘ └─┘ └──┘
src └──┘└──────────────┘└─┘ ┴ ┴ └┘└──────────────┘└─┘ ┴ ┴ └─
typ └──┘└──────────────┘└─┘└─┘┴└─┘┴└──┘└┘└──────────────┘└─┘└─┘┴└─┘┴└──┘└─
doc └──┘ └─┘ ┴ ┴ └┘ └─┘ ┴ ┴ └─
txt └──┘ └─┘ ┴ ┴ └┘ └─┘ ┴ ┴ └─
par └──┘ └─┘ ┴ ┴ └┘ └─┘ ┴ ┴ └─
pid └┘ └─┘ ┴ ┴ └┘ └─┘ ┴ ┴ └─
st └──────────────────────────────────┘└───────────────────────────────┘└─
379 ← _root_.pow_add, sum_mul_div_add_sum_mul_div_eq_mul _ hpq0, mul_comm]
id └────────────┘ └────────────────────────────────┘ └──┘ └──────┘
src ───┘└────────────┘└┘└────────────────────────────────┘└─┘ └┘└──────┘└─
typ ───┘└────────────┘└┘└────────────────────────────────┘└─┘└──┘└┘└──────┘└─
doc ───┘ └┘└────────────────────────────────┘└─┘ └┘ └─
txt ───┘ └┘ └─┘ └┘ └─
par ───┘ └┘ └─┘ └┘ └─
pid ───┘ └┘ └─┘ └┘ ┴└
st ─────────────────┘└─────────────────────────────────────────┘└────────┘┴└
380
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
381 lemma legendre_sym_two (hp1 : p % 2 = 1) : legendre_sym 2 p hp = (-1) ^ (p / 4 + p / 2) :=
id ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
382 have hp2 : p ≠ 2, from mt (congr_arg (% 2)) (by simp [hp1]),
id ┴ ┴ └┘ └───────┘ ┴ └─┘
src ┴ └┘ └───────┘ ┴ └────┘ ┴
typ ┴ ┴ └┘ └───────┘ ┴ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────┘
383 have hp22 : p / 2 / 2 = _ := div_eq_filter_card (show 0 < 2, from dec_trivial)
id ┴ ┴ ┴ ┴ └────────────────┘ ┴ └─────────┘
src ┴ ┴ ┴ └────────────────┘ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ └────────────────┘ ┴ └─────────┘
doc └─────────┘
384 (nat.div_le_self (p / 2) 2),
id └─────────────┘ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴
385 have hcard : (Ico 1 (p / 2).succ).card = p / 2, by simp,
id └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
src └─┘ ┴ └──┘ └──┘ ┴ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
doc └─┘ └──┘ └──┘
txt └──┘
par └──┘
st └───┘
386 have hx2 : ∀ x ∈ Ico 1 (p / 2).succ, (2 * x : zmodp p hp).val = 2 * x,
id ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴ └──┘ ┴ └───┘ └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴
doc └─┘
387 from λ x hx, have h2xp : 2 * x < p,
id ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴
388 from calc 2 * x ≤ 2 * (p / 2) : mul_le_mul_of_nonneg_left
id ┴ ┴ ┴ ┴ ┴ └───────────────────────┘
src ┴ ┴ ┴ └───────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └───────────────────────┘
389 (le_of_lt_succ $ by finish) dec_trivial
id └───────────┘ └─────────┘
src └───────────┘ └────┘ └─────────┘
typ └───────────┘ └────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘
par └────┘
st └─────┘
390 ... < _ : by conv_rhs {rw [← mod_add_div p 2, add_comm, hp1]}; exact lt_succ_self _,
id └─────────┘ ┴ └──────┘ └─┘ └──────────┘
src └────────┘└────┘└─────────┘┴ └──┘└──────┘└┘ ┴┴ └────┘└──────────┘└┘
typ └────────┘└────┘└─────────┘┴┴└──┘└──────┘└┘└─┘┴┴ └────┘└──────────┘└┘
doc └────┘ └┘
txt └────────┘└────┘ ┴ └──┘ └┘ ┴┴ └────┘ └┘
par └────────┘└────┘ ┴ └──┘ └┘ ┴┴ └────┘ └┘
pid ┴└─────┘ ┴ └──┘ └┘ └┘ ┴ └┘
st └─────────┘└──────────────────┘└─────────┘└───┘ └┘└───────────────────┘
391 by rw [← nat.cast_two, ← nat.cast_mul, zmodp.val_cast_of_lt _ h2xp],
id └──────────┘ └──────────┘ └──────────────────┘ └──┘
src └────┘└──────────┘└──┘└──────────┘└┘└──────────────────┘└─┘ ┴
typ └────┘└──────────┘└──┘└──────────┘└┘└──────────────────┘└─┘└──┘┴
doc └────┘ └──┘ └┘ └─┘ ┴
txt └────┘ └──┘ └┘ └─┘ ┴
par └────┘ └──┘ └┘ └─┘ ┴
pid └──┘ └──┘ └┘ └─┘ ┴
st └─────────────────┘└──────────────┘└───────────────────────────┘┴
392 have hdisj : disjoint
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
393 ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmodp p hp).val))
id └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘
src └─┘ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ └───┘ └─┘
typ └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘
doc └─┘ └────┘
394 ((Ico 1 (p / 2).succ).filter (λ x, x * 2 ≤ p / 2)),
id └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └────┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └────┘
395 from disjoint_filter.2 (λ x hx, by simp [hx2 _ hx, mul_comm]),
id └─────────────┘┴ ┴ └┘ └─┘ └┘ └──────┘
src └─────────────┘┴ └────┘ └─┘ └┘└──────┘┴
typ └─────────────┘┴ ┴ └┘ └────┘└─┘└─┘└┘└┘└──────┘┴
doc └────┘ └─┘ └┘ ┴
txt └────┘ └─┘ └┘ ┴
par └────┘ └─┘ └┘ ┴
pid ┴┴ └─┘ └┘ ┴
st └────────────────────────┘
396 have hunion :
397 ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmodp p hp).val)) ∪
id └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴
src └─┘ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴
typ └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴
doc └─┘ └────┘
398 ((Ico 1 (p / 2).succ).filter (λ x, x * 2 ≤ p / 2)) =
id └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └────┘
399 Ico 1 (p / 2).succ,
id └─┘ ┴ ┴ └──┘
src └─┘ ┴ └──┘
typ └─┘ ┴ ┴ └──┘
doc └─┘
400 begin
st └─────
401 rw [filter_union_right],
id └────────────────┘
src └──┘└────────────────┘┴
typ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────────┘└──
402 conv_rhs {rw [← @filter_true _ (Ico 1 (p / 2).succ)]},
id └─────────┘ └─┘ ┴ ┴
src └────────┘└────┘ └─────────┘└─┘ └─┘└─┘ ┴┴└────────┘┴
typ └────────┘└────┘ └─────────┘└─┘ └─┘└─┘ ┴┴┴└────────┘┴
doc └─┘
txt └────────┘└────┘ └─┘ └─┘ ┴ └────────┘┴
par └────────┘└────┘ └─┘ └─┘ ┴ └────────┘┴
pid ┴└─────┘ └─┘ └─┘ ┴ └─────────┘
st ─────────────┘└───────────────────────────────────────┘ └┘└
403 exact filter_congr (λ x hx, by simp [hx2 _ hx, lt_or_le, mul_comm])
id └──────────┘ └─┘ └┘ └──────┘ └──────┘
src └────┘└──────────┘┴ └─────┘ ┴└────┘ └─┘ └┘└──────┘└┘└──────┘┴└─
typ └────┘└──────────┘┴ └─────┘ ┴└────┘└─┘└─┘└┘└┘└──────┘└┘└──────┘┴└─
doc └────┘ ┴ └─────┘ ┴└────┘ └─┘ └┘ └┘ ┴└─
txt └────┘ ┴ └─────┘ ┴└────┘ └─┘ └┘ └┘ ┴└─
par └────┘ ┴ └─────┘ ┴└────┘ └─┘ └┘ └┘ ┴└─
pid ┴ ┴ └─────┘ └─────┘ └─┘ └┘ └┘ └┘└
st ─────────────────────────────────┘└──────────────────────────────────┘└─
404 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
405 begin
st └─────
406 rw [gauss_lemma _ hp1 (prime_ne_zero hp prime_two hp2),
id └─────────┘ └─┘ └───────────┘ └┘ └───────┘ └─┘
src └──┘└─────────┘└─┘ ┴ └───────────┘┴ ┴└───────┘┴ └──
typ └──┘└─────────┘└─┘└─┘┴ └───────────┘┴└┘┴└───────┘┴└─┘└──
doc └──┘└─────────┘└─┘ ┴ ┴ ┴ ┴ └──
txt └──┘ └─┘ ┴ ┴ ┴ ┴ └──
par └──┘ └─┘ ┴ ┴ ┴ ┴ └──
pid └┘ └─┘ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────────┘└─
407 neg_one_pow_eq_pow_mod_two, @neg_one_pow_eq_pow_mod_two _ _ (p / 4 + p / 2)],
id └────────────────────────┘ └────────────────────────┘ ┴ ┴
src ───┘└────────────────────────┘└┘ └────────────────────────┘└───┘ ┴ └─┘┴┴ ┴ └──┘
typ ───┘└────────────────────────┘└┘ └────────────────────────┘└───┘ ┴ └─┘┴┴┴┴ └──┘
doc ───┘ └┘ └───┘ ┴ └─┘ ┴ ┴ └──┘
txt ───┘ └┘ └───┘ ┴ └─┘ ┴ ┴ └──┘
par ───┘ └┘ └───┘ ┴ └─┘ ┴ ┴ └──┘
pid ───┘ └┘ └───┘ ┴ └─┘ ┴ ┴ └──┘
st ─────────────────────────────┘└───────────────────────────────────────────────┘└──
408 refine congr_arg2 _ rfl ((@zmod.eq_iff_modeq_nat 2 _ _).1 _),
id └────────┘ └─┘ └───────────────────┘
src └─────┘└────────┘└─┘└─┘┴ └───────────────────┘└──────────┘
typ └─────┘└────────┘└─┘└─┘┴ └───────────────────┘└──────────┘
doc └─────┘ └─┘ ┴ └──────────┘
txt └─────┘ └─┘ ┴ └──────────┘
par └─────┘ └─┘ ┴ └──────────┘
pid ┴ └─┘ ┴ └──────────┘
st ─────────────────────────────────────────────────────────────┘└─
409 rw [show 4 = 2 * 2, from rfl, ← nat.div_div_eq_div_mul, hp22, nat.cast_add,
id ┴ ┴ └─┘ └────────────────────┘ └──┘ └──────────┘
src └──┘ └─┘┴└─┘┴└───────┘└─┘└──┘└────────────────────┘└┘ └┘└──────────┘└─
typ └──┘ └─┘┴└─┘┴└───────┘└─┘└──┘└────────────────────┘└┘└──┘└┘└──────────┘└─
doc └──┘ └─┘ └─┘ └───────┘ └──┘ └┘ └┘ └─
txt └──┘ └─┘ └─┘ └───────┘ └──┘ └┘ └┘ └─
par └──┘ └─┘ └─┘ └───────┘ └──┘ └┘ └┘ └─
pid └┘ └─┘ └─┘ └───────┘ └──┘ └┘ └┘ └─
st ─────────────────────────────┘└────────────────────────┘└────┘└────────────┘└─
410 ← sub_eq_iff_eq_add', sub_eq_add_neg, zmod.neg_eq_self_mod_two,
id └────────────────┘ └────────────┘ └──────────────────────┘
src ─────┘└────────────────┘└┘└────────────┘└┘└──────────────────────┘└─
typ ─────┘└────────────────┘└┘└────────────┘└┘└──────────────────────┘└─
doc ─────┘ └┘ └┘ └─
txt ─────┘ └┘ └┘ └─
par ─────┘ └┘ └┘ └─
pid ─────┘ └┘ └┘ └─
st ───────────────────────┘└──────────────┘└────────────────────────┘└─
411 ← nat.cast_add, ← card_disjoint_union hdisj, hunion, hcard]
id └──────────┘ └─────────────────┘ └───┘ └────┘ └───┘
src ─────┘└──────────┘└──┘└─────────────────┘┴ └┘ └┘ └┘
typ ─────┘└──────────┘└──┘└─────────────────┘┴└───┘└┘└────┘└┘└───┘└┘
doc ─────┘ └──┘ ┴ └┘ └┘ └┘
txt ─────┘ └──┘ ┴ └┘ └┘ └┘
par ─────┘ └──┘ ┴ └┘ └┘ └┘
pid ─────┘ └──┘ ┴ └┘ └┘ ┴┴
st ─────────────────┘└───────────────────────────┘└──────┘└─────┘┴┴
412 end
st └─┘
413
414 lemma exists_pow_two_eq_two_iff (hp1 : p % 2 = 1) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
415 (∃ a : zmodp p hp, a ^ 2 = 2) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
id ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
416 have hp2 : ((2 : ℕ) : zmodp p hp) ≠ 0,
id ┴ └───┘ ┴ └┘ ┴
src ┴ └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
417 from zmodp.prime_ne_zero hp prime_two (λ h, by simp * at *),
id └─────────────────┘ └┘ └───────┘ ┴
src └─────────────────┘ └───────┘ └─────────┘
typ └─────────────────┘ └┘ └───────┘ ┴ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴┴┴└──┘
st └──────────┘
418 have hpm4 : p % 4 = p % 8 % 4, from (nat.mod_mul_left_mod p 2 4).symm,
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ └──┘
src ┴ ┴ ┴ ┴ └──────────────────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ └──┘
419 have hpm2 : p % 2 = p % 8 % 2, from (nat.mod_mul_left_mod p 4 2).symm,
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ └──┘
src ┴ ┴ ┴ ┴ └──────────────────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ └──┘
420 begin
st └─────
421 rw [show (2 : zmodp p hp) = (2 : ℕ), by simp, ← legendre_sym_eq_one_iff hp hp2,
id └───┘ ┴ └┘ ┴ └─────────────────────┘ └┘ └─┘
src └──┘ ┴ └──┘└───┘┴ ┴ └┘┴┴ └──┘ └────┘└──┘└──┘└─────────────────────┘┴ ┴ └─
typ └──┘ ┴ └──┘└───┘┴┴┴└┘└┘┴┴ └──┘ └────┘└──┘└──┘└─────────────────────┘┴└┘┴└─┘└─
doc └──┘ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ └────┘└──┘└──┘ ┴ ┴ └─
txt └──┘ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ └────┘└──┘└──┘ ┴ ┴ └─
par └──┘ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ └────┘└──┘└──┘ ┴ ┴ └─
pid └┘ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ └────────────┘ ┴ ┴ └─
st ────────────────────────────────────────┘└───┘└────────────────────────────────┘└─
422 legendre_sym_two hp hp1, neg_one_pow_eq_one_iff_even (show (-1 : ℤ) ≠ 1, from dec_trivial),
id └──────────────┘ └┘ └─┘ └─────────────────────────┘ ┴ ┴ └─────────┘
src ───┘└──────────────┘┴ ┴ └┘└─────────────────────────┘┴ ┴ ┴└──┘ └┘┴└───────┘└─────────┘└──
typ ───┘└──────────────┘┴└┘┴└─┘└┘└─────────────────────────┘┴ ┴ ┴└──┘ └┘┴└───────┘└─────────┘└──
doc ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └┘ └───────┘└─────────┘└──
txt ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └┘ └───────┘ └──
par ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └┘ └───────┘ └──
pid ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └┘ └───────┘ └──
st ──────────────────────────┘└─────────────────────────────────────────────────────────────────┘└─
423 even_add, even_div, even_div],
id └──────┘ └──────┘ └──────┘
src ───┘└──────┘└┘└──────┘└┘└──────┘┴
typ ───┘└──────┘└┘└──────┘└┘└──────┘┴
doc ───┘ └┘ └┘ ┴
txt ───┘ └┘ └┘ ┴
par ───┘ └┘ └┘ ┴
pid ───┘ └┘ └┘ ┴
st ───────────┘└────────┘└────────┘└──
424 have := nat.mod_lt p (show 0 < 8, from dec_trivial),
id └────────┘ ┴ ┴
src └──────┘└────────┘┴ ┴ └─┘┴└───────┘ ┴
typ └──────┘└────────┘┴┴┴ └─┘┴└───────┘ ┴
doc └──────┘ ┴ ┴ └─┘ └───────┘ ┴
txt └──────┘ ┴ ┴ └─┘ └───────┘ ┴
par └──────┘ ┴ ┴ └─┘ └───────┘ ┴
pid └───┘└─┘ ┴ ┴ └─┘ └───────┘ ┴
st ────────────────────────────────────────────────────┘└─
425 revert this hp1,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
426 erw [hpm4, hpm2],
id └──┘ └──┘
src └───┘ └┘ ┴
typ └───┘└──┘└┘└──┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────┘└────┘└──
427 generalize hm : p % 8 = m,
id ┴ ┴
src └──────────────┘ ┴┴└─┘ ┴
typ └──────────────┘┴┴┴└─┘ ┴
doc └──────────────┘ ┴ └─┘ ┴
txt └──────────────┘ ┴ └─┘ ┴
par └──────────────┘ ┴ └─┘ ┴
pid └─┘└┘┴ ┴ └─┘ ┴
st ──────────────────────────┘└─
428 clear hm,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ─────────┘└─
429 revert m,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
430 exact dec_trivial
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘
431 end
st └─┘
432
433 lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q % 2 = 1) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
434 (∃ a : zmodp p hp, a ^ 2 = q) ↔ ∃ b : zmodp q hq, b ^ 2 = p :=
id ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
435 if hpq : p = q then by resetI; subst hpq else
id └┘ ┴ ┴ ┴ └─┘
src └┘ ┴ └────┘ └────┘ ┴
typ └┘ ┴ ┴ ┴ └────┘ └────┘└─┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴
st └─────────────────┘
436 have h1 : ((p / 2) * (q / 2)) % 2 = 0,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
437 from (dvd_iff_mod_eq_zero _ _).1
id └─────────────────┘ ┴
src └─────────────────┘ ┴
typ └─────────────────┘ ┴
438 (dvd_mul_of_dvd_left ((dvd_iff_mod_eq_zero _ _).2 $
id └─────────────────┘ └─────────────────┘ ┴
src └─────────────────┘ └─────────────────┘ ┴
typ └─────────────────┘ └─────────────────┘ ┴
439 by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp1]; refl) _),
id └────────────────────┘ ┴ ┴ └─┘ └─┘
src └────┘└────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘ ┴ └──┘
typ └────┘└────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘└─┘┴ └──┘
doc └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
txt └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
par └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
pid └──┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴
st └───────────────────────────┘└────────────────────────┘└───┘┴└────┘
440 begin
st └─────
441 have := quadratic_reciprocity hp hq (odd_of_mod_four_eq_one hp1) hq1 hpq,
id └───────────────────┘ └┘ └┘ └────────────────────┘ └─┘ └─┘ └─┘
src └──────┘└───────────────────┘┴ ┴ ┴ └────────────────────┘┴ └┘ ┴
typ └──────┘└───────────────────┘┴└┘┴└┘┴ └────────────────────┘┴└─┘└┘└─┘┴└─┘
doc └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
442 rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym,
id └────────────────────────┘ └┘ └──────────┘ └──────────┘
src └──┘└────────────────────────┘└┘ └┘└──────────┘└┘└──────────┘└─
typ └──┘└────────────────────────┘└┘└┘└┘└──────────┘└┘└──────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ───────────────────────────────┘└──┘└────────────┘└────────────┘└─
443 if_neg (zmodp.prime_ne_zero hp hq hpq),
id └────┘ └─────────────────┘ └┘ └┘ └─┘
src ───┘└────┘┴ └─────────────────┘┴ ┴ ┴ └──
typ ───┘└────┘┴ └─────────────────┘┴└┘┴└┘┴└─┘└──
doc ───┘ ┴ ┴ ┴ ┴ └──
txt ───┘ ┴ ┴ ┴ ┴ └──
par ───┘ ┴ ┴ ┴ ┴ └──
pid ───┘ ┴ ┴ ┴ ┴ └──
st ─────────────────────────────────────────┘└─
444 if_neg (zmodp.prime_ne_zero hq hp (ne.symm hpq))] at this,
id └────┘ └─────────────────┘ └┘ └┘ └─────┘ └─┘
src ───┘└────┘┴ └─────────────────┘┴ ┴ ┴ └─────┘┴ └─────────┘
typ ───┘└────┘┴ └─────────────────┘┴└┘┴└┘┴ └─────┘┴└─┘└─────────┘
doc ───┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
par ───┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘
st ───────────────────────────────────────────────────┘┴└──────┘└─
445 split_ifs at this; simp *; contradiction
src └───────────────┘ └────┘ └────────────┘
typ └───────────────┘ └────┘ └────────────┘
doc └───────────────┘ └────┘ └────────────┘
txt └───────────────┘ └────┘ └────────────┘
par └───────────────┘ └────┘ └────────────┘
pid └──────┘ ┴┴ ┴
st ──────────────────────────────────────────┘
446 end
st └─┘
447
448 lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3)
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
449 (hq3 : q % 4 = 3) (hpq : p ≠ q) : (∃ a : zmodp p hp, a ^ 2 = q) ↔ ¬∃ b : zmodp q hq, b ^ 2 = p :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ └┘┴ ┴ ┴ ┴ ┴
450 have h1 : ((p / 2) * (q / 2)) % 2 = 1,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
451 from nat.odd_mul_odd
id └─────────────┘
src └─────────────┘
typ └─────────────┘
452 (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp3]; refl)
id └────────────────────┘ ┴ ┴ └─┘ └─┘
src └────┘└────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘ ┴ └──┘
typ └────┘└────────────────────┘└┘ └─┘┴└─┘┴└───────┘└─┘└┘└─┘┴ └──┘
doc └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
txt └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
par └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
pid └──┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴
st └───────────────────────────┘└────────────────────────┘└───┘┴└────┘
453 (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hq3]; refl),
id └────────────────────┘ └─┘ └─┘
src └────┘└────────────────────┘└┘ └─┘ └─┘ └───────┘└─┘└┘ ┴ └──┘
typ └────┘└────────────────────┘└┘ └─┘ └─┘ └───────┘└─┘└┘└─┘┴ └──┘
doc └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
txt └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
par └────┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴ └──┘
pid └──┘ └┘ └─┘ └─┘ └───────┘ └┘ ┴
st └───────────────────────────┘└────────────────────────┘└───┘┴└────┘
454 begin
st └─────
455 have := quadratic_reciprocity hp hq (odd_of_mod_four_eq_three hp3)
id └───────────────────┘ └┘ └┘ └─┘
src └──────┘└───────────────────┘┴ ┴ ┴ ┴ └─
typ └──────┘└───────────────────┘┴└┘┴└┘┴ ┴└─┘└─
doc └──────┘ ┴ ┴ ┴ ┴ └─
txt └──────┘ ┴ ┴ ┴ ┴ └─
par └──────┘ ┴ ┴ ┴ ┴ └─
pid └───┘└─┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────────
456 (odd_of_mod_four_eq_three hq3) hpq,
id └──────────────────────┘ └─┘ └─┘
src ───┘ └──────────────────────┘┴ └┘
typ ───┘ └──────────────────────┘┴└─┘└┘└─┘
doc ───┘ ┴ └┘
txt ───┘ ┴ └┘
par ───┘ ┴ └┘
pid ───┘ ┴ └┘
st ─────────────────────────────────────┘└─
457 rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym,
id └────────────────────────┘ └┘ └──────────┘ └──────────┘
src └──┘└────────────────────────┘└┘ └┘└──────────┘└┘└──────────┘└─
typ └──┘└────────────────────────┘└┘└┘└┘└──────────┘└┘└──────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ───────────────────────────────┘└──┘└────────────┘└────────────┘└─
458 if_neg (zmodp.prime_ne_zero hp hq hpq),
id └────┘ └─────────────────┘ └┘ └┘ └─┘
src ───┘└────┘┴ └─────────────────┘┴ ┴ ┴ └──
typ ───┘└────┘┴ └─────────────────┘┴└┘┴└┘┴└─┘└──
doc ───┘ ┴ ┴ ┴ ┴ └──
txt ───┘ ┴ ┴ ┴ ┴ └──
par ───┘ ┴ ┴ ┴ ┴ └──
pid ───┘ ┴ ┴ ┴ ┴ └──
st ─────────────────────────────────────────┘└─
459 if_neg (zmodp.prime_ne_zero hq hp hpq.symm)] at this,
id └────┘ └─────────────────┘ └┘ └┘ └──────┘
src ───┘└────┘┴ └─────────────────┘┴ ┴ ┴└──────┘└────────┘
typ ───┘└────┘┴ └─────────────────┘┴└┘┴└┘┴└──────┘└────────┘
doc ───┘ ┴ ┴ ┴ ┴ └────────┘
txt ───┘ ┴ ┴ ┴ ┴ └────────┘
par ───┘ ┴ ┴ ┴ ┴ └────────┘
pid ───┘ ┴ ┴ ┴ ┴ └┘└──────┘
st ──────────────────────────────────────────────┘┴└──────┘└─
460 split_ifs at this; simp *; contradiction
src └───────────────┘ └────┘ └────────────┘
typ └───────────────┘ └────┘ └────────────┘
doc └───────────────┘ └────┘ └────────────┘
txt └───────────────┘ └────┘ └────────────┘
par └───────────────┘ └────┘ └────────────┘
pid └──────┘ ┴┴ ┴
st ──────────────────────────────────────────┘
461 end
st └─┘
462
463 end zmodp